[proofplan] We verify each axiom of $\mathrm{ZFC}$ in the transitive rank-initial structure $V_\kappa$. The elementary axioms are inherited from the ambient universe once we know that $V_\kappa$ is transitive and closed under finite set formation, unions, and bounded definable subsets. The only substantial points are Power Set, Replacement, and Choice: in each case the strong limit property gives small cardinality below $\kappa$, and regularity bounds the ranks of fewer than $\kappa$ many objects below $\kappa$. [/proofplan]

[step:Record the closure properties of $V_\kappa$ below an inaccessible cardinal] For each ordinal $\alpha$, let $V_\alpha$ denote the $\alpha$th level of the cumulative hierarchy, and let $V_\kappa = \bigcup_{\alpha < \kappa} V_\alpha$. Since $\kappa$ is a limit ordinal, $V_\kappa$ is transitive. Indeed, if $x \in y \in V_\kappa$, then $y \in V_\alpha$ for some ordinal $\alpha < \kappa$, so every element of $y$ lies in some earlier rank $V_\beta$ with $\beta < \alpha$, hence $x \in V_\kappa$. We also use two standard consequences of strong inaccessibility. First, for every ordinal $\alpha < \kappa$, $|V_\alpha| < \kappa$. This follows by transfinite induction on $\alpha$: successor stages use that $\kappa$ is a strong limit cardinal, and limit stages below $\kappa$ use regularity of $\kappa$. Second, if $B$ is a set of ordinals below $\kappa$ and $|B| < \kappa$, then $\sup B < \kappa$, by regularity of $\kappa$. [/step]

[step:Verify the elementary axioms by transitivity and rank closure] Extensionality holds in $(V_\kappa,\in)$ because $V_\kappa$ is transitive and the membership relation is the ambient membership relation restricted to $V_\kappa$. Pairing holds as follows. If $x,y \in V_\kappa$, choose ordinals $\alpha,\beta < \kappa$ with $x \in V_\alpha$ and $y \in V_\beta$. Define $\gamma = \max\{\alpha,\beta\}+1$. Since $\kappa$ is a limit ordinal, $\gamma < \kappa$, and $\{x,y\} \subset V_\gamma$, so $\{x,y\} \in V_{\gamma+1} \subset V_\kappa$. Union holds similarly. If $a \in V_\kappa$, choose $\alpha < \kappa$ with $a \in V_\alpha$. Since every element of $a$ has rank below $\alpha$, every element of $\bigcup a$ has rank below $\alpha$, so $\bigcup a \subset V_\alpha$ and therefore $\bigcup a \in V_{\alpha+1} \subset V_\kappa$. Infinity holds because $\kappa$ is uncountable, so $\omega < \kappa$ and hence $\omega \in V_{\omega+1} \subset V_\kappa$. Foundation is inherited by every transitive class with the ambient membership relation: any nonempty $a \in V_\kappa$ has an ambient $\in$-minimal element, and that same element witnesses foundation inside $V_\kappa$. [/step]

[step:Obtain Separation by forming definable subclasses of existing sets] Let $a \in V_\kappa$, and let $\varphi(z,p_1,\dots,p_n)$ be any first-order formula in the language of set theory with parameters $p_1,\dots,p_n \in V_\kappa$. Define the set $ b = \{z \in a : (V_\kappa,\in) \models \varphi(z,p_1,\dots,p_n)\}$. This definition is made in the ambient universe, using the satisfaction relation for the set-sized structure $(V_\kappa,\in)$. Since $b \subset a$ and $a \in V_\kappa$, choose $\alpha < \kappa$ such that $a \subset V_\alpha$. Then $b \subset V_\alpha$, so $b \in V_{\alpha+1} \subset V_\kappa$. Thus the required separating subset exists inside $V_\kappa$. [/step]

[step:Verify Power Set by bounding the ranks of all subsets of a set] Let $x \in V_\kappa$. Choose an ordinal $\alpha < \kappa$ such that $x \subset V_\alpha$. If $y \subset x$, then $y \subset V_\alpha$, hence $y \in V_{\alpha+1}$. Therefore $\mathcal P(x) \subset V_{\alpha+1}$. It follows that $\mathcal P(x) \in V_{\alpha+2}$. Since $\kappa$ is a limit ordinal and $\alpha < \kappa$, we have $\alpha+2 < \kappa$, so $\mathcal P(x) \in V_\kappa$. This is exactly the power set required by the internal axiom of Power Set. [/step]

[step:Verify Replacement by bounding the ranks of a small definable image]Let $a \in V_\kappa$, let $p_1,\dots,p_n \in V_\kappa$ be parameters, and let $\varphi(u,v,p_1,\dots,p_n)$ be a formula such that $(V_\kappa,\in)$ satisfies that for every $u \in a$ there is a unique $v \in V_\kappa$ with $\varphi(u,v,p_1,\dots,p_n)$. Define the ambient set $Y = \{v \in V_\kappa : \text{for some } u \in a,\ (V_\kappa,\in) \models \varphi(u,v,p_1,\dots,p_n)\}$. Because the formula defines a function on $a$ inside $V_\kappa$, there is a surjection from $a$ onto $Y$, so $|Y| \le |a|$. Choose $\alpha < \kappa$ with $a \in V_\alpha$. Since $|V_\alpha| < \kappa$, we have $|a| < \kappa$, and hence $|Y| < \kappa$. For each $v \in Y$, let $\rho(v)$ be the rank of $v$. Define $R = \{\rho(v) : v \in Y\}$. Then $R \subset \kappa$ and $|R| < \kappa$. By regularity of $\kappa$, the ordinal $\beta = \sup\{\rho(v)+1 : v \in Y\}$ is still below $\kappa$. Thus $Y \subset V_\beta$, so $Y \in V_{\beta+1} \subset V_\kappa$. Therefore the replacement image exists in $V_\kappa$.[/step]

[guided]The only difficulty in Replacement is not forming the image in the ambient universe; the ambient universe already satisfies Replacement. The difficulty is proving that the image set has rank below $\kappa$, so that it belongs to $V_\kappa$. Let $a \in V_\kappa$, let $p_1,\dots,p_n \in V_\kappa$ be parameters, and suppose that a formula $\varphi(u,v,p_1,\dots,p_n)$ defines a function on $a$ inside $(V_\kappa,\in)$. This means that for every $u \in a$ there is exactly one $v \in V_\kappa$ such that $(V_\kappa,\in) \models \varphi(u,v,p_1,\dots,p_n)$. Define the image set in the ambient universe by $Y = \{v \in V_\kappa : \text{for some } u \in a,\ (V_\kappa,\in) \models \varphi(u,v,p_1,\dots,p_n)\}$. The satisfaction relation is legitimate here because $V_\kappa$ is a set, not a proper class. We first bound the cardinality of $Y$. Since the formula defines a function on $a$, each element of $Y$ is the value associated to at least one element of $a$, so $|Y| \le |a|$. Choose $\alpha < \kappa$ with $a \in V_\alpha$. Then $a \subset V_\alpha$, and the closure fact above gives $|V_\alpha| < \kappa$. Hence $|a| < \kappa$, and therefore $|Y| < \kappa$. Cardinality alone is not enough: a small subset of $V_\kappa$ could still have elements with ranks cofinal in $\kappa$ unless regularity prevents this. For each $v \in Y$, let $\rho(v)$ denote the rank of $v$, and define $R = \{\rho(v) : v \in Y\}$. Since every $v$ lies in $V_\kappa$, each $\rho(v)$ is below $\kappa$. Also $|R| \le |Y| < \kappa$. Regularity of $\kappa$ now gives $\sup\{\rho(v)+1 : v \in Y\} < \kappa$. Call this supremum $\beta$. Then every $v \in Y$ lies in $V_\beta$, so $Y \subset V_\beta$. Hence $Y \in V_{\beta+1}$, and because $\beta+1 < \kappa$, we conclude $Y \in V_\kappa$. Thus the image demanded by the Replacement axiom is not merely externally present; it is internally present as an element of $V_\kappa$.[/guided]

[step:Verify Choice by bounding an ambient choice function] Let $A \in V_\kappa$ be a set whose members are nonempty sets, as computed inside $V_\kappa$. By transitivity, each member of each $x \in A$ is also in $V_\kappa$, so nonemptiness is absolute between $V_\kappa$ and the ambient universe. By the ambient [Axiom of Choice](/page/Axiom%20of%20Choice), there exists a function $f$ with domain $A$ such that $f(x) \in x$ for every $x \in A$. We show that some such $f$ lies in $V_\kappa$. Choose $\alpha < \kappa$ such that $A \in V_\alpha$. Then every $x \in A$ lies in $V_\alpha$, and every chosen value $f(x) \in x$ lies in $V_\alpha$ by transitivity of $V_\alpha$ at the relevant lower ranks. The graph of $f$ is a set of ordered pairs $(x,f(x))$ indexed by $x \in A$. Since $|A| < \kappa$ and all entries of these ordered pairs have rank bounded below $\alpha+1$, the ranks of all ordered pairs in $f$ are bounded by some ordinal $\beta < \kappa$. Hence $f \subset V_\beta$ and $|f| < \kappa$, so $f \in V_{\beta+1} \subset V_\kappa$. Therefore $V_\kappa$ contains a choice function for $A$, and Choice holds in $(V_\kappa,\in)$. [/step]

[step:Conclude that every ZFC axiom holds in $V_\kappa$] The preceding steps verify Extensionality, Pairing, Union, Infinity, Foundation, Separation, Power Set, Replacement, and Choice in the structure $(V_\kappa,\in)$. Thus every axiom of $\mathrm{ZFC}$ is satisfied by $(V_\kappa,\in)$, and therefore $V_\kappa \models \mathrm{ZFC}$. [/step]