[proofplan] We verify the ZFC axioms inside the transitive rank segment $V_\kappa$. The easy axioms follow from transitivity and the fact that $\kappa$ is a limit ordinal, while Power Set follows by an explicit rank calculation. The key point for Replacement is that strong inaccessibility implies $|V_\alpha|<\kappa$ for every $\alpha<\kappa$, and regularity of $\kappa$ then bounds the ranks of all values of an internally definable function on a set $a\in V_\kappa$. Choice is checked by taking an ambient well-ordering of a set and observing that the well-ordering relation has rank below $\kappa$. [/proofplan]

[step:Establish transitivity and the basic rank closure of $V_\kappa$] 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 an ordinal, $V_\kappa$ is transitive: if $x\in y\in V_\kappa$, then $y\in V_\alpha$ for some $\alpha<\kappa$, so $y\subset V_\beta$ for some $\beta<\alpha$ when $\alpha$ is a successor, and in all cases every element of $y$ has rank $<\alpha<\kappa$; hence $x\in V_\kappa$. We shall use the following rank closure repeatedly. If $x_1,\dots,x_m\in V_\kappa$ is a finite list, choose ordinals $\alpha_1,\dots,\alpha_m<\kappa$ with $x_i\in V_{\alpha_i}$ for each $i\in\{1,\dots,m\}$. Define $\alpha=\sup\{\alpha_1,\dots,\alpha_m\}+m+3$. Because $\kappa$ is an uncountable limit ordinal, $\alpha<\kappa$. Thus any set obtained from $x_1,\dots,x_m$ by finitely many applications of pairing, ordered-pair formation, Cartesian product formation, union, or finite-rank power-set operations has rank below $\kappa$ and therefore belongs to $V_\kappa$. [/step]

[step:Show that all lower rank levels have size below $\kappa$]We prove by transfinite induction on $\alpha<\kappa$ that $|V_\alpha|<\kappa$. For $\alpha=0$, $V_0=\varnothing$, so $|V_0|=0<\kappa$. Suppose first that $\alpha=\beta+1$ and $|V_\beta|<\kappa$. Since $V_{\beta+1}=\mathcal P(V_\beta)$, we have \begin{align*} |V_{\beta+1}|=2^{|V_\beta|} \end{align*} Because $\kappa$ is a strong limit cardinal and $|V_\beta|<\kappa$, it follows that $2^{|V_\beta|}<\kappa$, hence $|V_{\beta+1}|<\kappa$. Now let $\lambda<\kappa$ be a nonzero limit ordinal and suppose $|V_\beta|<\kappa$ for every $\beta<\lambda$. Define a cardinal \begin{align*} \mu=\sup_{\beta<\lambda}|V_\beta| \end{align*} The indexing set $\lambda$ has cardinality $|\lambda|<\kappa$, and every cardinal in the displayed supremum is $<\kappa$. Since $\kappa$ is regular, the supremum of fewer than $\kappa$ many cardinals below $\kappa$ is still below $\kappa$, so $\mu<\kappa$. Since \begin{align*} V_\lambda=\bigcup_{\beta<\lambda}V_\beta \end{align*} there is a surjection from $\lambda\times \mu$ onto $V_\lambda$ after choosing injections $V_\beta\hookrightarrow\mu$ for each $\beta<\lambda$. Since $|\lambda|<\kappa$ and $\mu<\kappa$, cardinal arithmetic gives $|\lambda|\cdot\mu<\kappa$: for infinite factors this product is the maximum of the two factors, and the finite cases are smaller. Hence \begin{align*} |V_\lambda|\le |\lambda|\cdot\mu<\kappa \end{align*} Thus $|V_\alpha|<\kappa$ for every $\alpha<\kappa$.[/step]

[guided]The reason this size estimate is needed is Replacement: if a function is defined on a set $a\in V_\kappa$, we must know that $a$ has size $<\kappa$ before regularity can bound the ranks of all its images. We prove the estimate by induction on the rank level. At rank $0$, the level is empty: \begin{align*} V_0=\varnothing. \end{align*} Thus $|V_0|=0<\kappa$. For the successor step, assume $|V_\beta|<\kappa$. The next level is the power set: \begin{align*} V_{\beta+1}=\mathcal P(V_\beta). \end{align*} Therefore \begin{align*} |V_{\beta+1}|=2^{|V_\beta|}. \end{align*} Here the strong limit part of inaccessibility is used exactly: since $|V_\beta|<\kappa$, strong limit gives $2^{|V_\beta|}<\kappa$. Hence $|V_{\beta+1}|<\kappa$. For a limit ordinal $\lambda<\kappa$, the level $V_\lambda$ is the union of all previous levels: \begin{align*} V_\lambda=\bigcup_{\beta<\lambda}V_\beta. \end{align*} By the induction hypothesis, every $V_\beta$ has size below $\kappa$. Since the index set $\lambda$ also has size below $\kappa$, regularity of $\kappa$ implies that the supremum \begin{align*} \mu=\sup_{\beta<\lambda}|V_\beta| \end{align*} is still below $\kappa$. Choosing injections from each $V_\beta$ into a set of cardinality $\mu$, the union is bounded in size by $\lambda\times\mu$. The last inequality uses standard cardinal arithmetic: because both $|\lambda|$ and $\mu$ are below $\kappa$, their product is also below $\kappa$; if the relevant cardinals are infinite, the product is their maximum, and if they are finite the conclusion is immediate. Therefore \begin{align*} |V_\lambda|\le |\lambda|\cdot\mu<\kappa. \end{align*} This completes the induction and proves that every rank level below $\kappa$ has size below $\kappa$.[/guided]

[step:Verify the structural ZFC axioms inherited from transitivity] Extensionality holds in $(V_\kappa,\in)$ because membership between elements of $V_\kappa$ is the ambient membership relation: if $x,y\in V_\kappa$ have the same elements inside $V_\kappa$, then by transitivity all elements of $x$ and $y$ are already in $V_\kappa$, so $x$ and $y$ have the same ambient elements, hence $x=y$. Foundation holds because the ambient universe satisfies Foundation and $V_\kappa$ is transitive. If $a\in V_\kappa$ is nonempty, the ambient Foundation axiom gives an element $b\in a$ such that $b\cap a=\varnothing$. Since $a\subset V_\kappa$, this same $b$ is an $\in$-minimal element of $a$ inside $(V_\kappa,\in)$. Pairing holds by rank closure. If $x,y\in V_\kappa$, then the set $\{x,y\}$ has rank one larger than the maximum of the ranks of $x$ and $y$, hence belongs to $V_\kappa$. Union holds by rank closure. If $a\in V_\kappa$, choose $\alpha<\kappa$ with $a\in V_\alpha$. Since every element of every member of $a$ has rank below $\alpha$, the union $\bigcup a$ lies in $V_\alpha\subset V_\kappa$. Infinity holds because $\kappa$ is uncountable, hence $\omega<\kappa$. Therefore $\omega\in V_{\omega+1}\subset V_\kappa$, and $\omega$ is inductive inside $(V_\kappa,\in)$. [/step]

[step:Verify Separation for formulas with parameters from $V_\kappa$] Let $\varphi(z,p_1,\dots,p_m)$ be any first-order formula in the language of membership, let $p_1,\dots,p_m\in V_\kappa$ be parameters, and let $a\in V_\kappa$. Define the subset $b=\{z\in a:(V_\kappa,\in)\models\varphi(z,p_1,\dots,p_m)\}$. This set exists in the ambient universe by the ambient Separation axiom applied to $a$. Since $b\subset a$ and $a\in V_\kappa$, choose $\alpha<\kappa$ with $a\in V_\alpha$. Then $a\subset V_\beta$ for some $\beta<\alpha$ when $\alpha$ is successor, and in general every element of $a$ has rank $<\alpha$. Hence every element of $b$ has rank $<\alpha$, so $b\subset V_\alpha$ and therefore $b\in V_{\alpha+1}\subset V_\kappa$. Thus $(V_\kappa,\in)$ satisfies every instance of Separation. [/step]

[step:Verify Power Set by bounding the rank of every subset] Let $x\in V_\kappa$. Choose $\alpha<\kappa$ such that $x\in V_\alpha$. Then every element of $x$ has rank < $\alpha$, so every subset $y\subset x$ satisfies $y\subset V_\alpha$ and therefore $y\in V_{\alpha+1}$. Hence $\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 axiom inside $(V_\kappa,\in)$. [/step]

[step:Verify Replacement by regularity of $\kappa$] Let $\varphi(u,v,p_1,\dots,p_m)$ be a first-order formula in the language of membership, let $p_1,\dots,p_m\in V_\kappa$ be parameters, and let $a\in V_\kappa$. Assume that $(V_\kappa,\in)$ satisfies the functional condition $\forall u\in a\,\exists!v\in V_\kappa\,\varphi(u,v,p_1,\dots,p_m)$. For each $u\in a$, let $f(u)$ denote the unique element $v\in V_\kappa$ such that $(V_\kappa,\in)\models\varphi(u,v,p_1,\dots,p_m)$. Since $V_\kappa$ is a set in the ambient universe, the satisfaction relation for the set structure $(V_\kappa,\in)$ is first-order definable in the ambient universe. Hence the formula defining $f$ is an ambient first-order functional relation on the set $a$, and it defines a function $f:a\to V_\kappa$. For each $u\in a$, choose an ordinal $\rho(u)<\kappa$ such that $f(u)\in V_{\rho(u)}$. Since $a\in V_\kappa$, choose $\alpha<\kappa$ with $a\in V_\alpha$. By the previous size estimate, $|V_\alpha|<\kappa$, and since $a\subset V_\alpha$, we have $|a|<\kappa$. The set of ordinals $R=\{\rho(u):u\in a\}$ has cardinality at most $|a|$, hence cardinality $<\kappa$. Since $R\subset\kappa$ and $\kappa$ is regular, define $\beta=\sup R+1$. Then $\beta<\kappa$. For every $u\in a$, we have $\rho(u)<\beta$, so $f(u)\in V_\beta$. Therefore $f[a]=\{f(u):u\in a\}\subset V_\beta$. The ambient Replacement axiom gives the set $f[a]$, and since $f[a]\subset V_\beta$, we have $f[a]\in V_{\beta+1}\subset V_\kappa$. Thus the image set required by Replacement exists inside $(V_\kappa,\in)$. [/step]

[step:Verify Choice by placing an ambient well-ordering inside $V_\kappa$] Let $x\in V_\kappa$. By the ambient [Axiom of Choice](/page/Axiom%20of%20Choice), there exists a well-ordering relation $R\subset x\times x$ of $x$. Choose $\alpha<\kappa$ with $x\in V_\alpha$. Ordered pairs of elements of $x$ have rank bounded by $\alpha+3$, so $x\times x\in V_{\alpha+4}$. Since $R\subset x\times x$, the same rank bound gives $R\in V_{\alpha+5}$. Because $\kappa$ is a limit ordinal, $\alpha+5<\kappa$, hence $R\in V_\kappa$. Thus $(V_\kappa,\in)$ sees a well-ordering of every set $x\in V_\kappa$, so Choice holds in $(V_\kappa,\in)$. [/step]

[step:Conclude that $(V_\kappa,\in)$ satisfies ZFC] The preceding steps verify Extensionality, Foundation, Pairing, Union, Infinity, Separation, Power Set, Replacement, and Choice in the structure $(V_\kappa,\in)$. These are precisely the axioms and axiom schemes of ZFC. Therefore $(V_\kappa,\in)\models\mathrm{ZFC}$. This proves the theorem. [/step]