[proofplan] We verify the ZFC axioms in the transitive structure $M := (V_\kappa,\in)$. The elementary set-existence axioms are inherited from the ambient universe once we check that the relevant constructions remain below rank $\kappa$; this uses that $\kappa$ is a limit ordinal. Power Set is controlled by rank estimates, Replacement is controlled by regularity of $\kappa$, and Choice is obtained by taking an ambient well-ordering of each set and observing that its graph still has rank below $\kappa$. [/proofplan] [step:Fix the structure and record the rank bounds used throughout] Let $M$ denote the first-order structure $(V_\kappa,\in)$ in the language of set theory. Since $\kappa$ is strongly inaccessible, $\kappa$ is an uncountable regular limit cardinal. For each set $x$, let $\operatorname{rank}(x)$ denote the least ordinal $\alpha$ such that $x \subset V_\alpha$. Thus $x \in V_{\operatorname{rank}(x)+1}$. Since $V_\kappa = \bigcup_{\alpha<\kappa} V_\alpha$, every $x \in V_\kappa$ has $\operatorname{rank}(x) < \kappa$. We shall use the following elementary rank estimates. If $x,y \in V_\kappa$, then $\{x,y\} \in V_\kappa$. If $x \in V_\kappa$, then $\bigcup x \in V_\kappa$. If $x \in V_\kappa$, then $\mathcal{P}(x) \in V_\kappa$. Indeed, if $\operatorname{rank}(x),\operatorname{rank}(y)<\kappa$, then \begin{align*} \operatorname{rank}(\{x,y\}) \leq \max\{\operatorname{rank}(x),\operatorname{rank}(y)\}+1 < \kappa. \end{align*} If $\operatorname{rank}(x)=\alpha<\kappa$, then every element of $\bigcup x$ belongs to some element of $x$, so every element of $\bigcup x$ lies in $V_\alpha$; hence $\operatorname{rank}(\bigcup x)\leq \alpha<\kappa$. Finally, if $\operatorname{rank}(x)=\alpha<\kappa$, then every subset of $x$ is an element of $V_{\alpha+1}$, so \begin{align*} \mathcal{P}(x)\subset V_{\alpha+1}. \end{align*} Therefore $\operatorname{rank}(\mathcal{P}(x))\leq \alpha+1<\kappa$, and $\mathcal{P}(x)\in V_\kappa$. [guided] We first isolate the only set-theoretic bookkeeping that will be used repeatedly. Let $M := (V_\kappa,\in)$ be the membership structure whose universe is $V_\kappa$. Because $\kappa$ is strongly inaccessible, we may use that $\kappa$ is regular and a limit ordinal. For a set $x$, define $\operatorname{rank}(x)$ to be the least ordinal $\alpha$ such that $x \subset V_\alpha$. This convention gives $x \in V_{\operatorname{rank}(x)+1}$. Since $V_\kappa$ is the union of all $V_\alpha$ with $\alpha<\kappa$, every set in $V_\kappa$ has rank below $\kappa$. Now we check the closure facts. Suppose $x,y\in V_\kappa$. Then $\operatorname{rank}(x)<\kappa$ and $\operatorname{rank}(y)<\kappa$. The pair $\{x,y\}$ has rank at most one more than the larger of these two ranks: \begin{align*} \operatorname{rank}(\{x,y\}) \leq \max\{\operatorname{rank}(x),\operatorname{rank}(y)\}+1. \end{align*} Because $\kappa$ is a limit ordinal, this successor is still below $\kappa$. Hence $\{x,y\}\in V_\kappa$. If $x\in V_\kappa$ and $\operatorname{rank}(x)=\alpha<\kappa$, then each member of $x$ lies in $V_\alpha$. Every element of $\bigcup x$ is an element of some member of $x$, so it also lies below $V_\alpha$. Therefore \begin{align*} \operatorname{rank}(\bigcup x)\leq \alpha<\kappa. \end{align*} Thus $\bigcup x\in V_\kappa$. Finally, let $x\in V_\kappa$ and set $\alpha:=\operatorname{rank}(x)<\kappa$. Every subset $u\subset x$ has all its elements in $V_\alpha$, so $u\in V_{\alpha+1}$. Hence \begin{align*} \mathcal{P}(x)\subset V_{\alpha+1}. \end{align*} This implies $\operatorname{rank}(\mathcal{P}(x))\leq \alpha+1<\kappa$, again because $\kappa$ is a limit ordinal. Therefore $\mathcal{P}(x)\in V_\kappa$. [/guided] [/step] [step:Verify the structural axioms inherited from transitivity] The class $V_\kappa$ is transitive: if $x\in y\in V_\kappa$, then $x\in V_\kappa$. Indeed, if $y\in V_\alpha$ for some $\alpha<\kappa$, then every element of $y$ belongs to some $V_\beta$ with $\beta<\alpha$, hence belongs to $V_\kappa$. Extensionality holds in $M$ because membership in $M$ is the ambient membership relation restricted to a transitive set. If two elements of $V_\kappa$ have the same $M$-elements, then they have the same ambient elements, so they are equal by ambient Extensionality. Foundation holds in $M$ because any nonempty $a\in V_\kappa$ is a nonempty ambient set, and ambient Foundation gives an element $b\in a$ with $b\cap a=\varnothing$. Since $V_\kappa$ is transitive, this is exactly the assertion that $b$ has no $M$-element lying in $a$. [/step] [step:Verify pairing union infinity and power set by rank closure] Pairing holds in $M$ by the rank estimate from the first step: for all $x,y\in V_\kappa$, the set $\{x,y\}$ belongs to $V_\kappa$ and has exactly the required members. Union holds in $M$ because for every $x\in V_\kappa$, the ambient union $\bigcup x$ belongs to $V_\kappa$ and satisfies the union axiom with respect to the restricted membership relation. Let $\omega$ denote the first infinite ordinal, that is, the set of natural numbers. Infinity holds in $M$ because $\omega\in V_\kappa$. Since $\kappa$ is inaccessible, it is uncountable, so $\omega<\kappa$. Hence $\omega\in V_{\omega+1}\subset V_\kappa$, and the usual inductive-set witness for Infinity belongs to $M$. Power Set holds in $M$ because for every $x\in V_\kappa$, the ambient power set $\mathcal{P}(x)$ belongs to $V_\kappa$. Since $V_\kappa$ is transitive, the subsets of $x$ computed in $M$ are exactly the ambient subsets of $x$ that lie in $V_\kappa$; the previous rank estimate shows that every ambient subset of $x$ lies in $V_\kappa$. Therefore $\mathcal{P}(x)$ is the power set of $x$ inside $M$. [/step] [step:Verify separation by relativizing formulas to $V_\kappa$] Let $\varphi(z,p_1,\dots,p_n)$ be any formula in the language of set theory, let $a,p_1,\dots,p_n\in V_\kappa$, and define the ambient set \begin{align*} b:=\{z\in a : M\models \varphi(z,p_1,\dots,p_n)\}. \end{align*} This set exists by ambient Separation, since the satisfaction relation for the fixed set structure $M=(V_\kappa,\in)$ and the fixed formula $\varphi$ is definable by recursion on formulas. Because $b\subset a$ and $a\in V_\kappa$, transitivity and the rank estimate for subsets give $b\in \mathcal{P}(a)\in V_\kappa$. Thus $b$ is available inside $M$ and is exactly the subset of $a$ cut out by $\varphi$ in $M$. Hence $M$ satisfies the full Separation schema. [/step] [step:Verify replacement using regularity of $\kappa$ to bound the image ranks] Let $\varphi(x,y,p_1,\dots,p_n)$ be any formula, and let $a,p_1,\dots,p_n\in V_\kappa$. Assume that $M$ satisfies \begin{align*} \forall x\in a\,\exists!y\,\varphi(x,y,p_1,\dots,p_n). \end{align*} Define an ambient function \begin{align*} F:a&\to V_\kappa \end{align*} by letting $F(x)$ be the unique $y\in V_\kappa$ such that $M\models \varphi(x,y,p_1,\dots,p_n)$. Ambient Replacement gives the image set \begin{align*} B:=F[a]=\{F(x):x\in a\}. \end{align*} For each $x\in a$, define \begin{align*} \rho(x):=\operatorname{rank}(F(x)). \end{align*} Since $F(x)\in V_\kappa$, we have $\rho(x)<\kappa$ for all $x\in a$. The set $a$ has cardinality less than $\kappa$: indeed $a\in V_\kappa$, so $a\subset V_\alpha$ for some $\alpha<\kappa$, and strong inaccessibility gives $|V_\alpha|<\kappa$. Thus $\rho[a]$ is a set of fewer than $\kappa$ ordinals below $\kappa$. By regularity of $\kappa$, \begin{align*} \beta:=\sup\{\rho(x)+1:x\in a\}<\kappa. \end{align*} Then every element of $B$ lies in $V_\beta$, so $B\subset V_\beta$ and therefore $B\in V_{\beta+1}\subset V_\kappa$. Thus the image set required by Replacement belongs to $M$, and $M$ satisfies the full Replacement schema. [guided] Replacement is the only axiom where closure under finitely many rank operations is not enough. We must prove that a whole definable image of a set still has rank bounded below $\kappa$. Fix a formula $\varphi(x,y,p_1,\dots,p_n)$ and parameters $a,p_1,\dots,p_n\in V_\kappa$. Assume that inside $M$ the formula defines a unique output for each input in $a$: \begin{align*} M\models \forall x\in a\,\exists!y\,\varphi(x,y,p_1,\dots,p_n). \end{align*} Define the ambient function \begin{align*} F:a&\to V_\kappa \end{align*} by sending each $x\in a$ to the unique $y\in V_\kappa$ such that $M\models \varphi(x,y,p_1,\dots,p_n)$. This is a genuine set function in the ambient universe: the domain $a$ is a set, the structure $M$ is a set structure, and the defining satisfaction relation is fixed. By ambient Replacement, the image \begin{align*} B:=F[a]=\{F(x):x\in a\} \end{align*} is a set. The remaining question is not whether $B$ exists in $V$; it does. The question is whether $B$ has rank below $\kappa$, so that $B\in V_\kappa$. For each $x\in a$, define the ordinal \begin{align*} \rho(x):=\operatorname{rank}(F(x)). \end{align*} Because $F(x)\in V_\kappa$, each $\rho(x)$ is below $\kappa$. We now need one ordinal below $\kappa$ that bounds all these ranks at once. This is where regularity of $\kappa$ enters. First, $a$ has size less than $\kappa$. To see this, choose $\alpha<\kappa$ with $a\subset V_\alpha$. Since $\kappa$ is strongly inaccessible, the cumulative level $V_\alpha$ has cardinality less than $\kappa$, and therefore $|a|<\kappa$. Hence the set of ordinals \begin{align*} \{\rho(x)+1:x\in a\} \end{align*} has cardinality less than $\kappa$ and is contained in $\kappa$. Since $\kappa$ is regular, its supremum is still below $\kappa$. Define \begin{align*} \beta:=\sup\{\rho(x)+1:x\in a\}. \end{align*} Then $\beta<\kappa$. Now every $F(x)$ has rank strictly below $\beta$, so every $F(x)$ belongs to $V_\beta$. Therefore \begin{align*} B\subset V_\beta. \end{align*} This means $B\in V_{\beta+1}$, and because $\beta+1<\kappa$, we get $B\in V_\kappa$. Thus the required replacement image exists inside $M$. [/guided] [/step] [step:Verify choice by putting a well-ordering relation below $\kappa$] Let $x\in V_\kappa$. By ambient Choice, there exists a relation $R\subset x\times x$ that well-orders $x$. We show $R\in V_\kappa$. Choose $\alpha<\kappa$ such that $x\in V_\alpha$. For every $u,v\in x$, the ordered pair $(u,v)$, coded as $\{\{u\},\{u,v\}\}$, has rank bounded by $\alpha+2$. Hence \begin{align*} x\times x\subset V_{\alpha+3}. \end{align*} Since $R\subset x\times x$, we have $R\subset V_{\alpha+3}$, so $R\in V_{\alpha+4}\subset V_\kappa$. Therefore $M$ contains a well-ordering of every set $x\in M$, and so $M$ satisfies Choice. [/step] [step:Conclude that every axiom of ZFC holds in $V_\kappa$] We have verified Extensionality, Foundation, Pairing, Union, Infinity, Power Set, Separation, Replacement, and Choice inside $M=(V_\kappa,\in)$. These are precisely the axioms and axiom schemas of ZFC. Therefore \begin{align*} (V_\kappa,\in)\models \mathrm{ZFC}. \end{align*} This completes the proof. [/step]