[proofplan] We verify each axiom of $\mathrm{ZFC}$ inside the structure $(V_\kappa,\in)$. The basic axioms follow from the fact that $V_\kappa$ is transitive and that $\kappa$ is a limit ordinal, so $V_\kappa$ is closed under finite rank constructions. The two rank-sensitive axioms are Power Set and Replacement: Power Set is bounded below $\kappa$ using the strong limit property, and Replacement is bounded below $\kappa$ using regularity. Finally, Choice is inherited from the ambient universe because every set in $V_\kappa$ has a well-order whose graph still has rank below $\kappa$. [/proofplan]

[step:Establish transitivity and basic closure of $V_\kappa$]Let $\omega$ denote the least infinite ordinal, and for any set $s$ let $\mathcal{P}(s)$ denote the set of all subsets of $s$. Since $\kappa$ is an uncountable regular strong limit cardinal, in particular $\kappa$ is a limit ordinal and $\omega < \kappa$. Recall that \begin{align*} V_\kappa = \bigcup_{\alpha < \kappa} V_\alpha . \end{align*} If $x \in V_\kappa$, choose an ordinal $\alpha < \kappa$ such that $x \in V_\alpha$. Since the cumulative hierarchy is increasing and transitive at each stage, every $y \in x$ belongs to some $V_\beta$ with $\beta < \alpha$, hence $y \in V_\kappa$. Thus $V_\kappa$ is transitive. We record the finite closure needed below. If $x,y \in V_\kappa$, choose $\alpha,\beta < \kappa$ with $x \in V_\alpha$ and $y \in V_\beta$. Let $\gamma = \max\{\alpha,\beta\}+3$. Since $\kappa$ is a limit ordinal, $\gamma < \kappa$. The Kuratowski ordered pair $(x,y) := \{\{x\},\{x,y\}\}$ belongs to $V_\gamma$, and therefore $(x,y) \in V_\kappa$. The same rank estimate gives $\{x,y\} \in V_\kappa$, $x \cup y \in V_\kappa$, and, for each $x \in V_\kappa$, $\bigcup x \in V_\kappa$. We also fix the rank notation used below. For any set $z$, let $\operatorname{rank}(z)$ denote the least ordinal $\rho$ such that $z \subset V_\rho$; equivalently, $z \in V_{\rho+1}$. We will use the standard induction on $\alpha < \kappa$ showing that $|V_\alpha| < \kappa$ for every $\alpha < \kappa$: successor stages use $|V_{\alpha+1}| = 2^{|V_\alpha|} < \kappa$ by the strong limit property, and limit stages use regularity of $\kappa$ to bound the union of fewer than $\kappa$ many sets, each of cardinality less than $\kappa$. Hence every $z \in V_\kappa$ has cardinality less than $\kappa$.[/step]

[guided]We first isolate the structural fact that makes the easy axioms easy: $V_\kappa$ is transitive. By definition, \begin{align*} V_\kappa = \bigcup_{\alpha < \kappa} V_\alpha . \end{align*} Thus, if $x \in V_\kappa$, then $x \in V_\alpha$ for some ordinal $\alpha < \kappa$. The hierarchy is built by repeatedly taking power sets, so elements of elements appearing before stage $\alpha$ already appear at earlier stages. Hence for every $y \in x$ there is an ordinal $\beta < \alpha$ such that $y \in V_\beta$. Since $\beta < \alpha < \kappa$, we get $y \in V_\kappa$. This proves transitivity. Next we check the finite constructions explicitly, because these are the rank estimates used by Pairing, Union, ordered pairs, products, and Choice. Suppose $x,y \in V_\kappa$. Choose ordinals $\alpha,\beta < \kappa$ such that $x \in V_\alpha$ and $y \in V_\beta$. Define \begin{align*} \gamma = \max\{\alpha,\beta\}+3 . \end{align*} Because $\kappa$ is inaccessible, it is a limit ordinal, so adding finitely many successor stages below $\kappa$ remains below $\kappa$; hence $\gamma < \kappa$. The singleton $\{x\}$, the pair $\{x,y\}$, and the Kuratowski ordered pair \begin{align*} (x,y) := \{\{x\},\{x,y\}\} \end{align*} all occur by stage $V_\gamma$. Therefore these objects lie in $V_\kappa$. The same finite-rank calculation shows that $x \cup y \in V_\kappa$, and if $x \in V_\kappa$, then $\bigcup x \in V_\kappa$ because every element of every element of $x$ already lies below the rank of $x$. Finally, we define the rank notation that will appear in the rank-bounding arguments. For any set $z$, $\operatorname{rank}(z)$ means the least ordinal $\rho$ such that $z \subset V_\rho$; equivalently, $z \in V_{\rho+1}$. We also need the size estimate $|V_\alpha| < \kappa$ for every $\alpha < \kappa$. This follows by induction on $\alpha$. At a successor stage, if $|V_\alpha| < \kappa$, then \begin{align*} |V_{\alpha+1}| = |\mathcal{P}(V_\alpha)| = 2^{|V_\alpha|} < \kappa, \end{align*} because $\kappa$ is a strong limit cardinal. At a limit stage $\lambda < \kappa$, the set $V_\lambda$ is the union of the family $(V_\alpha)_{\alpha < \lambda}$, which has fewer than $\kappa$ many members, each of cardinality less than $\kappa$ by the induction hypothesis. Since $\kappa$ is regular, this union has cardinality less than $\kappa$. Therefore every $z \in V_\kappa$ belongs to some $V_\alpha$ with $\alpha < \kappa$, and hence $|z| \le |V_\alpha| < \kappa$.[/guided]

[step:Verify the axioms inherited from transitivity and finite closure] Extensionality holds in $(V_\kappa,\in)$ because equality and membership are the ambient equality and membership, and $V_\kappa$ is transitive. Foundation holds because any nonempty $a \in V_\kappa$ is a nonempty ambient set, so the ambient Foundation axiom gives an element $b \in a$ with $a \cap b = \varnothing$; transitivity ensures the same witness is seen inside $V_\kappa$. Pairing holds by the finite closure proved above: for $x,y \in V_\kappa$, the set $\{x,y\}$ lies in $V_\kappa$. Union holds because for $x \in V_\kappa$, the set $\bigcup x$ lies in $V_\kappa$. Infinity holds because $\omega \in V_{\omega+1}$ and $\omega+1 < \kappa$, so $\omega \in V_\kappa$. Separation holds as follows. Let $a \in V_\kappa$, and let $\varphi(u,p_1,\dots,p_n)$ be any formula in the language of set theory with parameters $p_1,\dots,p_n \in V_\kappa$. Because $V_\kappa$ is a set, the satisfaction relation for the set-sized first-order structure $(V_\kappa,\in)$ is definable in the ambient universe by recursion on formulas. Define, in the ambient universe, \begin{align*} b = \{u \in a : (V_\kappa,\in) \models \varphi(u,p_1,\dots,p_n)\}. \end{align*} By ambient Separation, $b$ is a set. Since $b \subset a$ and $a \in V_\kappa$, the rank of $b$ is at most the rank of $a$, so $b \in V_\kappa$. Hence the subset required by Separation exists inside $V_\kappa$. [/step]

[step:Use the strong limit property to verify Power Set]Let $x \in V_\kappa$. Choose an ordinal $\alpha < \kappa$ such that $x \in V_\alpha$. Then $x \subset V_\alpha$, so every subset of $x$ belongs to $V_{\alpha+1}$. Therefore \begin{align*} \mathcal{P}(x) \subset V_{\alpha+1}. \end{align*} By the rank-size estimate proved in the first step, $x \in V_\kappa$ implies $|x| < \kappa$. Since $\kappa$ is a strong limit cardinal, we obtain \begin{align*} |\mathcal{P}(x)| = 2^{|x|} < \kappa . \end{align*} Each element of $\mathcal{P}(x)$ has rank below $\alpha+1 < \kappa$, and there are fewer than $\kappa$ such elements. By regularity of $\kappa$, their ranks are bounded by some ordinal $\delta < \kappa$. Thus $\mathcal{P}(x) \subset V_\delta$, so $\mathcal{P}(x) \in V_{\delta+1} \subset V_\kappa$. This is exactly the Power Set axiom inside $(V_\kappa,\in)$.[/step]

[guided]We must show that if $x$ is an element of $V_\kappa$, then the full power set $\mathcal{P}(x)$ is also an element of $V_\kappa$. Choose an ordinal $\alpha < \kappa$ such that $x \in V_\alpha$. Since elements of $V_\alpha$ are subsets of earlier stages of the hierarchy, every subset of $x$ has rank below $\alpha+1$. Equivalently, \begin{align*} \mathcal{P}(x) \subset V_{\alpha+1}. \end{align*} This tells us that the elements of $\mathcal{P}(x)$ individually have rank below $\kappa$, but we also need the set $\mathcal{P}(x)$ itself to appear before stage $\kappa$. For that, we use the cardinal assumptions. The first step proved the needed size estimate: $|V_\alpha| < \kappa$ for every $\alpha < \kappa$, and hence every $x \in V_\kappa$ has $|x| < \kappa$. Because $\kappa$ is a strong limit cardinal, \begin{align*} |\mathcal{P}(x)| = 2^{|x|} < \kappa . \end{align*} Thus $\mathcal{P}(x)$ is a set of fewer than $\kappa$ many objects, each of rank below $\kappa$. Now regularity supplies the uniform rank bound. The collection of ranks of elements of $\mathcal{P}(x)$ has cardinality less than $\kappa$, and every one of those ranks is below $\kappa$. Since $\kappa$ is regular, the supremum of this collection is still some ordinal $\delta < \kappa$. Hence every subset of $x$ belongs to $V_\delta$, so \begin{align*} \mathcal{P}(x) \subset V_\delta . \end{align*} Therefore $\mathcal{P}(x) \in V_{\delta+1}$, and because $\delta+1 < \kappa$, we conclude $\mathcal{P}(x) \in V_\kappa$. This proves Power Set in $V_\kappa$.[/guided]

[step:Use regularity to verify Replacement] Let $a \in V_\kappa$, let $p_1,\dots,p_n \in V_\kappa$, and let $\varphi(u,v,p_1,\dots,p_n)$ be a formula such that $(V_\kappa,\in)$ satisfies \begin{align*} \forall u \in a \, \exists! v \, \varphi(u,v,p_1,\dots,p_n). \end{align*} Because $V_\kappa$ is a set, the satisfaction relation for first-order formulas over the structure $(V_\kappa,\in)$ is definable in the ambient universe by recursion on formulas. Define the ambient functional relation $\Theta(u,v)$ to mean that $v \in V_\kappa$ and $(V_\kappa,\in)\models \varphi(u,v,p_1,\dots,p_n)$. The displayed hypothesis says that for every $u \in a$ there exists a unique ambient set $v$ such that $\Theta(u,v)$ holds. Applying ambient Replacement to the definable functional relation $\Theta$ on the set $a$, we obtain the image set \begin{align*} b = \{v \in V_\kappa : \exists u \in a \text{ such that } (V_\kappa,\in)\models \varphi(u,v,p_1,\dots,p_n)\}. \end{align*} For each $u \in a$, let $v_u$ denote the unique element of $V_\kappa$ satisfying $(V_\kappa,\in)\models \varphi(u,v_u,p_1,\dots,p_n)$. Since $a \in V_\kappa$, the rank-size estimate gives $|a| < \kappa$. The set of ranks \begin{align*} R = \{\operatorname{rank}(v_u) : u \in a\} \end{align*} has cardinality at most $|a|$, hence cardinality less than $\kappa$. Also $R \subset \kappa$ because each $v_u \in V_\kappa$. By regularity of $\kappa$, there is an ordinal $\delta < \kappa$ such that $\operatorname{rank}(v_u) < \delta$ for every $u \in a$. Hence $b \subset V_\delta$, so $b \in V_{\delta+1} \subset V_\kappa$. Thus the required replacement image exists inside $V_\kappa$. [/step]

[step:Use ambient choice and the proved Power Set closure to verify Choice inside $V_\kappa$] Let $x \in V_\kappa$. By the ambient [Axiom of Choice](/page/Axiom%20of%20Choice), there exists a well-order relation $R \subset x \times x$ on $x$. Let $\rho = \operatorname{rank}(x)$. Since $x \in V_\kappa$, we have $\rho < \kappa$. If $a,b \in x$, then $a,b \in V_\rho$, so the Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$ belongs to $V_{\rho+3}$. Hence $x \times x \subset V_{\rho+3}$, and therefore $x \times x \in V_{\rho+4} \subset V_\kappa$, because $\kappa$ is a limit ordinal. By the Power Set axiom already verified inside $(V_\kappa,\in)$, the set $\mathcal{P}(x \times x)$ belongs to $V_\kappa$. Since $R \in \mathcal{P}(x \times x)$ and $V_\kappa$ is transitive, we have $R \in V_\kappa$. Therefore $V_\kappa$ contains a well-order of every one of its sets. Hence $(V_\kappa,\in)$ satisfies the [Well-Ordering Theorem](/theorems/1227) form of Choice, and therefore satisfies Choice. [/step]

[step:Conclude that every ZFC axiom holds in $(V_\kappa,\in)$] The previous steps verify Extensionality, Foundation, Pairing, Union, Infinity, Separation, Power Set, Replacement, and Choice in the structure $(V_\kappa,\in)$. These are precisely the axioms of $\mathrm{ZFC}$ in the usual first-order language of set theory. Therefore \begin{align*} (V_\kappa,\in) \models \mathrm{ZFC}. \end{align*} This proves the theorem. [/step]