[proofplan] We first recall the structural properties of the constructible hierarchy: each level is transitive, the hierarchy is increasing, and every ordinal appears in $L$. Let $V$ denote the ambient universe of sets in which the constructible hierarchy is being formed. These facts give that $L$ is a transitive proper class containing all ordinals, and they also make Extensionality and Foundation absolute from $V$ to $L$. The remaining axioms are verified by showing that the relevant sets are first-order definable over sufficiently large constructible levels. The non-formal parts of the argument are isolated in standard external metatheorems about $L$: the finite reflection theorem for formulas over $L$, the condensation-derived boundedness theorems for constructible subsets and definable images, and the uniform definability of the canonical Gödel well-order of $L$. These metatheorems are invoked here as established ingredients rather than reproved in full; the proof verifies exactly how their hypotheses apply. [/proofplan]

[step:Build the structural properties of the constructible hierarchy] For every ordinal $\alpha$, define $\operatorname{Def}(L_\alpha)$ to be the set of all subsets of $L_\alpha$ first-order definable over the structure $(L_\alpha,\in)$ with parameters from $L_\alpha$. The constructible hierarchy is the class function $\alpha\mapsto L_\alpha$ defined by transfinite recursion as follows: \begin{align*} L_0&=\varnothing,\\ L_{\alpha+1}&=\operatorname{Def}(L_\alpha),\\ L_\lambda&=\bigcup_{\alpha<\lambda}L_\alpha\quad\text{for limit ordinals }\lambda. \end{align*} We prove simultaneously by transfinite induction on $\beta$ that $L_\beta$ is transitive and that $L_\alpha\subseteq L_\beta$ whenever $\alpha\leq\beta$. For $\beta=0$, both assertions are immediate because $L_0=\varnothing$. Suppose first that $\beta=\gamma+1$ and the two assertions hold at stage $\gamma$. To prove $L_\gamma\subseteq L_{\gamma+1}$, let $x\in L_\gamma$. Since $L_\gamma$ is transitive, every element of $x$ belongs to $L_\gamma$, so $x\subseteq L_\gamma$. Therefore $x$ is the subset of $L_\gamma$ defined over $(L_\gamma,\in)$ from the parameter $x$ by the formula $z\in x$. Hence $x\in\operatorname{Def}(L_\gamma)=L_{\gamma+1}$. If $\alpha<\gamma$, the induction hypothesis gives $L_\alpha\subseteq L_\gamma\subseteq L_{\gamma+1}$, so monotonicity holds at $\gamma+1$. To prove transitivity at $\gamma+1$, let $x\in y\in L_{\gamma+1}$. Since $y\in\operatorname{Def}(L_\gamma)$, the set $y$ is a subset of $L_\gamma$. Thus $x\in L_\gamma\subseteq L_{\gamma+1}$. Now let $\beta=\lambda$ be a limit ordinal and assume the two assertions hold below $\lambda$. By definition, \begin{align*} L_\lambda=\bigcup_{\alpha<\lambda}L_\alpha. \end{align*} If $\alpha<\lambda$, then $L_\alpha\subseteq L_\lambda$, and monotonicity for pairs below $\lambda$ gives $L_\alpha\subseteq L_\rho$ whenever $\alpha\leq\rho<\lambda$. Hence monotonicity holds at $\lambda$. If $x\in y\in L_\lambda$, choose $\alpha<\lambda$ with $y\in L_\alpha$. Transitivity of $L_\alpha$ gives $x\in L_\alpha\subseteq L_\lambda$, so $L_\lambda$ is transitive. Finally, every ordinal belongs to $L$. We prove by transfinite induction on the ordinal $\alpha$ that $L_\alpha\cap\operatorname{Ord}=\alpha$. The base and limit cases follow from the displayed recursion and monotonicity. At the successor stage, the induction hypothesis gives $L_\alpha\cap\operatorname{Ord}=\alpha$. Since $L_\alpha$ is transitive, the elements of $L_\alpha$ satisfying the first-order formula "$z$ is an ordinal" form exactly the set $\alpha$. Hence $\alpha$ is first-order definable over $(L_\alpha,\in)$ without parameters, so $\alpha\in\operatorname{Def}(L_\alpha)=L_{\alpha+1}$. Also no ordinal $\xi>\alpha$ lies in $L_{\alpha+1}$, because every element of $L_{\alpha+1}$ is a subset of $L_\alpha$ and therefore has all ordinal members below $\alpha$. Thus $L_{\alpha+1}\cap\operatorname{Ord}=\alpha+1$. It follows that every ordinal $\alpha$ belongs to $L_{\alpha+1}\subset L$. [/step]

[step:Conclude that $L$ is a transitive proper class containing all ordinals] Since each $L_\alpha$ is transitive and the hierarchy is increasing, the union \begin{align*} L=\bigcup_{\alpha\in\operatorname{Ord}}L_\alpha \end{align*} is transitive: if $x\in y\in L$, then $y\in L_\alpha$ for some ordinal $\alpha$, and transitivity of $L_\alpha$ gives $x\in L_\alpha\subset L$. The previous step gives $\operatorname{Ord}\subset L$. Therefore $L$ cannot be a set, because if $L$ were a set, then $\operatorname{Ord}$ would be a subset of a set and hence a set, contradicting the [Burali-Forti theorem](/page/Burali-Forti%20Theorem) that the class of all ordinals is not a set. Thus $L$ is a proper class. [/step]

[step:Verify Extensionality and Foundation by transitivity] Extensionality holds in $(L,\in)$ because membership in $L$ is the actual membership relation restricted to $L$. If $x,y\in L$ and $x$ and $y$ have the same elements in $L$, then transitivity of $L$ implies that all elements of $x$ and $y$ are already in $L$, so $x$ and $y$ have the same elements in $V$. By Extensionality in $V$, $x=y$. Foundation holds in $(L,\in)$ because $L$ is transitive. If $a\in L$ is nonempty in $L$, then $a$ is nonempty in $V$. By Foundation in $V$, there is $x\in a$ such that $x\cap a=\varnothing$. Since $a\in L$ and $L$ is transitive, every element of $a$ belongs to $L$, so this same $x$ witnesses Foundation inside $(L,\in)$. [/step]

[step:Produce Pairing Union Infinity and Separation inside $L$] Let $a,b\in L$. Choose ordinals $\alpha,\beta$ such that $a\in L_\alpha$ and $b\in L_\beta$, and let $\gamma$ be an ordinal with $\alpha,\beta<\gamma$. The set $\{a,b\}$ is definable over $L_\gamma$ from parameters $a$ and $b$ by the formula $z=a\lor z=b$. Hence $\{a,b\}\in L_{\gamma+1}\subset L$, proving Pairing. Let $a\in L$, and choose an ordinal $\alpha$ such that $a\in L_\alpha$. Since $L_\alpha$ is transitive, every member of every member of $a$ lies in $L_\alpha$. The union $\bigcup a$ is definable over $L_\alpha$ from parameter $a$ by \begin{align*} z\in \bigcup a \iff \exists y\in a\,(z\in y). \end{align*} Thus $\bigcup a\in L_{\alpha+1}\subset L$, proving Union. Let $\omega$ denote the first infinite ordinal, equivalently the set of all finite ordinals. Infinity holds because $\omega$ is an ordinal and every ordinal belongs to $L$. Since $L$ is transitive, $(\omega,\in)$ computed in $L$ is the usual set of finite ordinals. For Separation, let $a\in L$, let $p_1,\dots,p_n\in L$ be parameters, and let $\varphi(x,p_1,\dots,p_n)$ be a first-order formula in the language of set theory. Choose an ordinal $\alpha$ such that $a,p_1,\dots,p_n\in L_\alpha$. Define \begin{align*} b=\{x\in a:(L,\in)\models \varphi(x,p_1,\dots,p_n)\}. \end{align*} We use the following precise form of the [finite reflection theorem for $L$](/page/Reflection%20Principle): for every finite set $\Sigma$ of first-order formulas and every set $A\subset L$, there is an ordinal $\beta$ such that $A\subseteq L_\beta$ and, for every formula $\psi\in\Sigma$ and every tuple of parameters from $A$ of the appropriate length, truth of $\psi$ in $(L,\in)$ is equivalent to truth of $\psi$ in $(L_\beta,\in)$. Apply this with $A=a\cup\{a,p_1,\dots,p_n\}$ and with $\Sigma$ equal to a finite reflection fragment containing $\varphi$ and the finitely many subformulas required by the Tarski recursion for that fixed formula. This is a finite absoluteness requirement for the given formula, not an assertion that a global satisfaction predicate for $L$ is definable in $L$. Because $a\in L$ and $L$ is transitive, every possible element $x\in a$ also belongs to $L$, so the set $A$ contains both the set parameter $a$ and all element-parameters over which Separation ranges. This gives a single ordinal $\beta>\alpha$ such that $a,p_1,\dots,p_n\in L_\beta$, every $x\in a$ lies in $L_\beta$, and, for every $x\in a$, \begin{align*} (L,\in)\models \varphi(x,p_1,\dots,p_n) \iff (L_\beta,\in)\models \varphi(x,p_1,\dots,p_n). \end{align*} Since $L_\beta$ is a set-sized structure, satisfaction for the fixed finite list $\Sigma$ is definable in the ambient universe by recursion on formula complexity. Therefore $b$ is first-order definable over $(L_\beta,\in)$ from parameters $a,p_1,\dots,p_n$, and hence $b\in L_{\beta+1}\subset L$. [/step]

[step:Bound constructible subsets to prove the internal Power Set axiom] Let $a\in L$. Choose an ordinal $\alpha$ such that $a\in L_\alpha$. We must show that the collection \begin{align*} \mathcal P^L(a)=\{x\in L:x\subseteq a\} \end{align*} belongs to $L$. We import the following standard bounded-subset theorem, proved from the [Condensation Lemma for $L$](/page/Condensation%20Lemma): for every $a\in L$ there is an ordinal $\beta(a)$ such that, for every $x\subseteq a$, if $x\in L$, then $x\in L_{\beta(a)}$. Its hypotheses apply because $a$ is a set of $L$. This is a substantial condensation theorem about the constructible hierarchy, not a routine closure observation. This bounded-subset theorem is used here as a prior metatheorem, not as a result proved by the following sketch. The point of this form is that the bound depends only on $a$, not on the particular definition or construction parameters for $x$. The condensation proof fixes a sufficiently closed constructible level and takes elementary Skolem hulls, using the canonical Skolem functions for the reflected finite fragments, generated by $\operatorname{tc}(a)\cup\{a\}$ together with the finitely many construction parameters needed for a candidate constructible subset $x\subseteq a$, where $\operatorname{tc}(a)$ denotes the [transitive closure](/theorems/1493) of $a$. Because every such $x$ is a subset of the fixed set $a$, the relevant traces on $a$ are coded by subsets of a set, and the hulls needed to realise those traces are represented by a set-indexed family of Skolem hulls. For each hull in this family, let $\eta$ denote the ordinal obtained as the height of its transitive collapse. The [Mostowski collapse](/page/Mostowski%20Collapse), together with condensation, identifies each collapse with an initial segment $L_\eta$ and sends the copy of $x$ back to the original subset of $a$. Hence every constructible subset of $a$ appears in one of these set-indexed initial segments, and the supremum of the corresponding successor ordinals gives a single ordinal bound depending only on $a$. Choose an ordinal $\beta$ such that $\beta(a)<\beta$ and $\alpha<\beta$. Then $a\in L_\beta$ by monotonicity, and every constructible subset of $a$ belongs to $L_\beta$ by the choice of $\beta(a)$. Hence \begin{align*} \mathcal P^L(a)=\{x\in L_\beta:x\subseteq a\}. \end{align*} The right-hand side is definable over $(L_\beta,\in)$ from the parameter $a$, which is an element of $L_\beta$, by the formula “$x\subseteq a$”. Therefore $\mathcal P^L(a)\in L_{\beta+1}\subset L$, so $(L,\in)$ satisfies Power Set internally. [/step]

[step:Use reflection and condensation to prove Replacement] Let $a\in L$, let $p_1,\dots,p_n\in L$, and suppose that a formula $\varphi(x,y,p_1,\dots,p_n)$ defines a function on $a$ inside $(L,\in)$; that is, for every $x\in a$ there is a unique $y\in L$ such that \begin{align*} (L,\in)\models \varphi(x,y,p_1,\dots,p_n). \end{align*} We must prove that the image set \begin{align*} b=\{y\in L:\exists x\in a\,(L,\in)\models \varphi(x,y,p_1,\dots,p_n)\} \end{align*} belongs to $L$. Apply the following standard bounded-image theorem, proved from the [finite reflection theorem for $L$](/page/Reflection%20Principle) and the [Condensation Lemma for $L$](/page/Condensation%20Lemma): if $a,p_1,\dots,p_n\in L$ and a formula $\varphi(x,y,p_1,\dots,p_n)$ defines a single-valued class function on $a$ over $(L,\in)$, then there is an ordinal $\beta$ such that every value of that function belongs to $L_\beta$. The hypotheses are exactly the displayed uniqueness assumption and the fact that $a,p_1,\dots,p_n$ are sets in $L$. This is a substantial reflection-and-condensation theorem supplying a uniform rank bound for all values at once. This bounded-image theorem is imported here as a prior metatheorem. It is a uniform condensation theorem, not a choice of a new reflected level for each individual $x$. More precisely, after fixing the finite list of formulas expressing existence and uniqueness for $\varphi$, reflection supplies constructible levels in which that finite fragment is absolute for the parameters $a,p_1,\dots,p_n$ and elements of $a$. The associated canonical Skolem functions are fixed for that finite fragment. Taking Skolem hulls generated by finite tuples from the set $a\cup\{a,p_1,\dots,p_n\}$ gives a set-indexed family of hulls. For each hull in this family, let $\eta$ denote the ordinal height of its transitive collapse; by the [Mostowski collapse](/page/Mostowski%20Collapse) and condensation, that collapse is the initial segment $L_\eta$. Since the indexing data are set-sized, the collection of these ordinals $\eta$ is bounded by a single ordinal. The uniqueness clause ensures that each value $y$ of the class function appears in one of those collapsed initial segments, so all values lie in one common $L_\beta$. Choose the resulting ordinal $\beta$. Then every value $y$ satisfying $\varphi(x,y,p_1,\dots,p_n)$ for some $x\in a$ lies in $L_\beta$, so \begin{align*} b=\{y\in L_\beta:\exists x\in a\,(L,\in)\models \varphi(x,y,p_1,\dots,p_n)\}. \end{align*} Choose an ordinal $\alpha$ such that $a,p_1,\dots,p_n\in L_\alpha$. By the [finite reflection theorem for $L$](/page/Reflection%20Principle) applied to the finite set consisting of $\varphi$ and its relevant subformulas, choose an ordinal $\delta$ such that $\alpha<\delta$, $\beta<\delta$, and truth of $\varphi(x,y,p_1,\dots,p_n)$ for all $x\in a$ and all $y\in L_\beta$ is equivalent in $(L,\in)$ and $(L_\delta,\in)$. Then $a,p_1,\dots,p_n,L_\beta\in L_\delta$: the original parameters are in $L_\delta$ by monotonicity, and $L_\beta\in L_{\beta+1}\subseteq L_\delta$ because $\beta<\delta$. Since $L_\delta$ is set-sized, satisfaction for this finite list of formulas is definable by recursion on formula complexity. Hence $b$ is definable over $L_\delta$ from parameters $a,p_1,\dots,p_n,L_\beta$, and so $b\in L_{\delta+1}\subset L$. Thus $(L,\in)$ satisfies Replacement. [/step]

[step:Define the canonical well-order of $L$ and obtain Choice] Fix once and for all a primitive recursive Gödel coding of first-order formulas by elements of $\omega$. Also fix a uniform set-theoretic coding of finite tuples: a tuple $(s_0,\dots,s_{k-1})$ is represented by the function with domain $k=\{0,\dots,k-1\}$ sending $i$ to $s_i$, equivalently by its graph of Kuratowski ordered pairs. Thus, for each ordinal $\alpha$, the assertion that $s$ is a finite tuple from $L_\alpha$ means that $s$ is a function whose domain is some finite ordinal $k\in\omega$ and whose range is contained in $L_\alpha$. For each ordinal $\alpha$, the satisfaction relation for the set-sized structure $(L_\alpha,\in)$ and a fixed formula code is definable in the ambient universe by recursion on formula complexity. Thus the relation \begin{align*} R(\alpha,e,s,x) \end{align*} meaning "$e$ is a formula code, $s$ is a finite tuple from $L_\alpha$, and the formula coded by $e$ with parameters $s$ defines $x$ as a subset of $L_\alpha$ over $(L_\alpha,\in)$" is uniform in $\alpha$. Use the standard [canonical Gödel well-order theorem for $L$](/page/Constructible%20Universe): the uniform relation $R$ induces a first-order definable class well-order $<_L$ of $L$ by comparing the least construction data. Explicitly, the construction datum of $x\in L$ is the lexicographically least triple $(\alpha,e,s)$ such that $x\in L_{\alpha+1}$ and $R(\alpha,e,s,x)$. The lexicographic comparison is fixed as follows: ordinals are compared by $\in$, formula codes are compared by the usual order on $\omega$, and tuple codes are compared first by length and then lexicographically coordinate-by-coordinate using the already defined $<_L$ on entries of lower construction rank. The cited theorem asserts that this recursive comparison is well-founded, uniform in the construction rank, and first-order definable over $L$ by a parameter-free formula in the language of set theory; it is proved by induction on constructible rank using the definability of satisfaction for each set-sized $L_\alpha$ and the fixed coding of formula and tuple data. Let $\theta(u,v)$ denote this fixed parameter-free formula, so that, for all $u,v\in L$, \begin{align*} u<_L v\iff (L,\in)\models \theta(u,v). \end{align*} Therefore $<_L$ is a first-order definable class relation on $L$ and well-orders $L$: every nonempty subclass of $L$ has elements of least construction ordinal, and among those elements the fixed well-order of formula codes and tuple codes gives a least construction datum. Now let $a\in L$ be a set whose elements are nonempty sets in $L$. For each $x\in a$, let $m_x$ denote the $<_L$-least element of $x$, which exists because $<_L$ well-orders $L$ and $x$ is a nonempty subset of $L$. Let $(u,v)$ denote the Kuratowski ordered pair $\{\{u\},\{u,v\}\}$. By Pairing, Union, Power Set, and Separation inside $L$, the Cartesian product $a\times\bigcup a$ belongs to $L$: it is the subset of $\mathcal P^L(\mathcal P^L(a\cup\bigcup a))$ consisting of Kuratowski pairs $(x,z)$ with $x\in a$ and $z\in\bigcup a$. Define \begin{align*} f=\{(x,z)\in a\times \bigcup a:z\in x\ \text{and}\ (L,\in)\models \neg\exists w\in x\,\theta(w,z)\}. \end{align*} The displayed definition uses only the first-order language of set theory, the set parameters $a$ and $\bigcup a$, and the fixed parameter-free formula $\theta$ defining $<_L$. Hence Separation in $L$ applies to the ambient set $a\times\bigcup a$, and the set $f$ belongs to $L$. For each $x\in a$ there is exactly one $z$ with $(x,z)\in f$, namely $z=m_x$, so $f$ is a choice function with domain $a$. Hence $(L,\in)$ satisfies Choice. [/step]

[step:Assemble the axioms of ZFC inside $L$] The Empty Set axiom holds because $\varnothing=L_0$ and $L_0\in L_1\subset L$. The preceding steps show that $(L,\in)$ satisfies Extensionality, Foundation, Pairing, Union, Infinity, Separation, Power Set, Replacement, and Choice. Therefore $(L,\in)$ satisfies all axioms of ZFC. Since $L$ is transitive, contains every ordinal, and is a proper class, $L$ is an inner model of ZFC. [/step]