[proofplan]
We prove, by transfinite induction on $\alpha$, the stronger simultaneous assertion that the ordinals appearing in $L_\alpha$ are exactly the smaller ordinals and that $\alpha$ itself appears at the next constructible stage. The key point is that $L_\alpha \cap \operatorname{Ord}$ is definable over $L_\alpha$: inside a transitive set, being an ordinal is expressed by the first-order condition that the set and all its elements are transitive. Therefore $L_\alpha \cap \operatorname{Ord} = \alpha$ belongs to $\operatorname{Def}(L_\alpha)=L_{\alpha+1}$.
[/proofplan]
[step:State the simultaneous induction property]
For each ordinal $\alpha$, let $P(\alpha)$ be the assertion
\begin{align*}
L_\alpha \cap \operatorname{Ord} = \alpha
\quad\text{and}\quad
\alpha \in L_{\alpha+1}.
\end{align*}
We prove $P(\alpha)$ for every ordinal $\alpha$ by transfinite induction.
We use the standard recursive definition of the constructible hierarchy:
\begin{align*}
L_0 &= \varnothing,\\
L_{\beta+1} &= \operatorname{Def}(L_\beta),\\
L_\lambda &= \bigcup_{\beta < \lambda} L_\beta
\quad\text{for limit ordinals }\lambda,
\end{align*}
and $L=\bigcup_{\beta\in\operatorname{Ord}}L_\beta$. We also use the standard monotonicity of the hierarchy: if $\beta \leq \alpha$, then $L_\beta \subseteq L_\alpha$.
[guided]
For each ordinal $\alpha$, we prove two facts at once:
\begin{align*}
L_\alpha \cap \operatorname{Ord} = \alpha
\quad\text{and}\quad
\alpha \in L_{\alpha+1}.
\end{align*}
The first statement says that at stage $\alpha$, the constructible hierarchy contains exactly the ordinals below $\alpha$. The second says that once stage $\alpha$ has been built, the ordinal $\alpha$ itself is constructed at the next stage.
The hierarchy is defined recursively by
\begin{align*}
L_0 &= \varnothing,\\
L_{\beta+1} &= \operatorname{Def}(L_\beta),\\
L_\lambda &= \bigcup_{\beta < \lambda} L_\beta
\quad\text{for limit ordinals }\lambda.
\end{align*}
Thus $L_{\beta+1}$ consists of the subsets of $L_\beta$ that are first-order definable over the structure $(L_\beta,\in)$, possibly with parameters from $L_\beta$. In particular, every element of $L_{\beta+1}=\operatorname{Def}(L_\beta)$ is a subset of $L_\beta$. The monotonicity property $L_\beta \subseteq L_\alpha$ for $\beta \leq \alpha$ follows directly from this recursive construction, and it is the mechanism that lets ordinals constructed at earlier stages remain present at all later stages.
[/guided]
[/step]
[step:Show that every smaller ordinal lies in $L_\alpha$]
Assume $P(\beta)$ holds for every ordinal $\beta < \alpha$. Let $\gamma < \alpha$ be an ordinal. By the induction hypothesis applied to $\gamma$,
\begin{align*}
\gamma \in L_{\gamma+1}.
\end{align*}
Since $\gamma+1 \leq \alpha$, monotonicity gives $L_{\gamma+1}\subseteq L_\alpha$. Hence $\gamma\in L_\alpha$. Therefore
\begin{align*}
\alpha \subseteq L_\alpha \cap \operatorname{Ord}.
\end{align*}
[guided]
Take an arbitrary ordinal $\gamma < \alpha$. The induction hypothesis applies at the earlier stage $\gamma$, so it gives
\begin{align*}
\gamma \in L_{\gamma+1}.
\end{align*}
Because $\gamma < \alpha$, we have $\gamma+1 \leq \alpha$. [Monotonicity of the constructible hierarchy](/theorems/4850) therefore gives
\begin{align*}
L_{\gamma+1}\subseteq L_\alpha.
\end{align*}
Combining these two facts yields $\gamma\in L_\alpha$. Since $\gamma$ was an arbitrary ordinal below $\alpha$, every element of $\alpha$ belongs to $L_\alpha$ and is an ordinal. Thus
\begin{align*}
\alpha \subseteq L_\alpha \cap \operatorname{Ord}.
\end{align*}
[/guided]
[/step]
[step:Show that no ordinal at stage $L_\alpha$ is at least $\alpha$]
Let $\gamma \in L_\alpha \cap \operatorname{Ord}$. If $\alpha=0$, then $L_0=\varnothing$, so there is no such $\gamma$. Assume $\alpha>0$.
If $\alpha$ is a limit ordinal, then $L_\alpha=\bigcup_{\delta<\alpha}L_\delta$. Hence there is an ordinal $\delta<\alpha$ such that $\gamma\in L_\delta$. By the induction hypothesis applied to $\delta$,
\begin{align*}
L_\delta\cap\operatorname{Ord}=\delta.
\end{align*}
Since $\gamma$ is an ordinal and $\gamma\in L_\delta$, we have $\gamma\in\delta$, and therefore $\gamma<\delta<\alpha$.
If $\alpha$ is a successor ordinal, write $\alpha=\delta+1$ for the unique ordinal $\delta$. Since $L_{\delta+1}=\operatorname{Def}(L_\delta)$, every element of $L_{\delta+1}$ is a subset of $L_\delta$. Thus $\gamma\subseteq L_\delta$. Because $\gamma$ is an ordinal, every $\eta\in\gamma$ is an ordinal, so
\begin{align*}
\gamma\subseteq L_\delta\cap\operatorname{Ord}.
\end{align*}
By the induction hypothesis applied to $\delta$,
\begin{align*}
L_\delta\cap\operatorname{Ord}=\delta.
\end{align*}
Hence $\gamma\subseteq\delta$. Since $\gamma$ and $\delta$ are ordinals, $\gamma\subseteq\delta$ implies $\gamma\leq\delta<\delta+1=\alpha$.
Therefore
\begin{align*}
L_\alpha \cap \operatorname{Ord} \subseteq \alpha.
\end{align*}
[guided]
Now suppose $\gamma \in L_\alpha \cap \operatorname{Ord}$. We must prove $\gamma<\alpha$.
If $\alpha=0$, then $L_0=\varnothing$, so no such $\gamma$ exists. Assume $\alpha>0$. There are two cases, and the successor case is the important one because we cannot use the induction hypothesis at the current stage $\alpha$.
First suppose $\alpha$ is a limit ordinal. By the recursive definition of the constructible hierarchy,
\begin{align*}
L_\alpha=\bigcup_{\delta<\alpha}L_\delta.
\end{align*}
Thus $\gamma\in L_\delta$ for some ordinal $\delta<\alpha$. The induction hypothesis applies to this earlier ordinal $\delta$ and gives
\begin{align*}
L_\delta\cap\operatorname{Ord}=\delta.
\end{align*}
Since $\gamma$ is an ordinal and belongs to $L_\delta$, it follows that $\gamma\in L_\delta\cap\operatorname{Ord}=\delta$. Therefore $\gamma<\delta<\alpha$.
Now suppose $\alpha$ is a successor ordinal. Write $\alpha=\delta+1$ for the unique ordinal $\delta$. Here we must not invoke $P(\delta+1)$, because $P(\alpha)$ is exactly the assertion being proved. Instead we use the definition of the successor level:
\begin{align*}
L_{\delta+1}=\operatorname{Def}(L_\delta).
\end{align*}
By definition, every element of $\operatorname{Def}(L_\delta)$ is a subset of $L_\delta$. Since $\gamma\in L_{\delta+1}$, this gives
\begin{align*}
\gamma\subseteq L_\delta.
\end{align*}
Because $\gamma$ is an ordinal, each element $\eta\in\gamma$ is also an ordinal. Hence every element of $\gamma$ belongs to $L_\delta\cap\operatorname{Ord}$, so
\begin{align*}
\gamma\subseteq L_\delta\cap\operatorname{Ord}.
\end{align*}
The induction hypothesis applies to $\delta<\alpha$ and gives
\begin{align*}
L_\delta\cap\operatorname{Ord}=\delta.
\end{align*}
Therefore $\gamma\subseteq\delta$. For ordinals, inclusion is the same as the non-strict order, so $\gamma\leq\delta$. Since $\delta<\delta+1=\alpha$, we obtain $\gamma<\alpha$.
Thus every ordinal contained in $L_\alpha$ is strictly below $\alpha$, and therefore
\begin{align*}
L_\alpha \cap \operatorname{Ord} \subseteq \alpha.
\end{align*}
[/guided]
[/step]
[step:Define $\alpha$ over $L_\alpha$ as the set of internal ordinals]
Combining the two inclusions gives
\begin{align*}
L_\alpha \cap \operatorname{Ord}=\alpha.
\end{align*}
Consider the first-order formula $\varphi(x)$ in the language of set theory saying:
\begin{align*}
x\text{ is transitive and every element of }x\text{ is transitive}.
\end{align*}
Since each $L_\alpha$ is transitive, for every $x\in L_\alpha$ the structure $(L_\alpha,\in)$ satisfies $\varphi(x)$ exactly when $x$ is an ordinal. Hence the subset of $L_\alpha$ defined over $(L_\alpha,\in)$ by $\varphi$ is
\begin{align*}
\{x\in L_\alpha : (L_\alpha,\in)\models \varphi(x)\}
=
L_\alpha\cap\operatorname{Ord}
=
\alpha.
\end{align*}
By the definition of the next constructible level,
\begin{align*}
\alpha \in \operatorname{Def}(L_\alpha)=L_{\alpha+1}.
\end{align*}
[guided]
We have proved both inclusions, so
\begin{align*}
L_\alpha \cap \operatorname{Ord}=\alpha.
\end{align*}
It remains to show that this set belongs to the next level $L_{\alpha+1}$.
The next level is
\begin{align*}
L_{\alpha+1}=\operatorname{Def}(L_\alpha),
\end{align*}
so it is enough to show that the subset $L_\alpha\cap\operatorname{Ord}$ is first-order definable over $(L_\alpha,\in)$. Use the first-order formula $\varphi(x)$ asserting that $x$ is transitive and every element of $x$ is transitive. Externally, this is exactly the usual von Neumann characterization of ordinals.
Because $L_\alpha$ is transitive, bounded membership facts about elements of elements of $L_\alpha$ are absolute between $L_\alpha$ and the ambient universe. Therefore, for $x\in L_\alpha$,
\begin{align*}
(L_\alpha,\in)\models \varphi(x)
\quad\Longleftrightarrow\quad
x\in\operatorname{Ord}.
\end{align*}
Thus the subset of $L_\alpha$ defined by $\varphi$ is
\begin{align*}
\{x\in L_\alpha : (L_\alpha,\in)\models \varphi(x)\}
=
L_\alpha\cap\operatorname{Ord}
=
\alpha.
\end{align*}
Since definable subsets of $L_\alpha$ are precisely the elements of $\operatorname{Def}(L_\alpha)$, we conclude
\begin{align*}
\alpha \in \operatorname{Def}(L_\alpha)=L_{\alpha+1}.
\end{align*}
[/guided]
[/step]
[step:Conclude that every ordinal belongs to $L$]
The preceding steps prove $P(\alpha)$ for the arbitrary ordinal $\alpha$. Hence, for every ordinal $\alpha$,
\begin{align*}
\alpha \in L_{\alpha+1}.
\end{align*}
Since $L=\bigcup_{\beta\in\operatorname{Ord}}L_\beta$ and $\alpha+1$ is an ordinal, it follows that $\alpha\in L$. Therefore
\begin{align*}
\operatorname{Ord}\subset L.
\end{align*}
This proves that every ordinal is constructible.
[/step]
