[proofplan]
We argue by the model-theoretic form of relative consistency. Assuming $\mathsf{ZFC}$ is consistent, the [Gödel Completeness Theorem](/theorems/4652) gives a model $M \models \mathsf{ZFC}$. Inside $M$, form the constructible universe $L^M$; the previously established constructibility theorems say that $L^M$ satisfies every axiom of $\mathsf{ZFC}$ and also satisfies $V=L$. Hence $\mathsf{ZFC}+V=L$ has a model, so by soundness it is syntactically consistent.
[/proofplan]
[step:Pass from syntactic consistency of $\mathsf{ZFC}$ to a model of $\mathsf{ZFC}$]
Assume that $\mathsf{ZFC}$ is syntactically consistent. By the Gödel Completeness Theorem for first-order logic, syntactic consistency of a first-order theory implies satisfiability; that is, there exists a first-order structure $M$ in the language $\{\in\}$ such that
\begin{align*}
M \models \mathsf{ZFC}.
\end{align*}
(citing a result not yet in the wiki: Gödel Completeness Theorem)
[guided]
The hypothesis is a syntactic one: there is no formal derivation of a contradiction from the axioms of $\mathsf{ZFC}$. To turn this into a semantic object, we use the Gödel Completeness Theorem for first-order logic. Applied to the first-order theory $\mathsf{ZFC}$ in the language with one binary relation symbol $\in$, it says that if $\mathsf{ZFC}$ is syntactically consistent, then $\mathsf{ZFC}$ has a model.
Therefore there exists a first-order structure $M$ for the language $\{\in\}$ such that
\begin{align*}
M \models \mathsf{ZFC}.
\end{align*}
This model is the ambient object in which we will build the constructible hierarchy.
(citing a result not yet in the wiki: Gödel Completeness Theorem)
[/guided]
[/step]
[step:Construct the internal constructible universe $L^M$]
Inside the model $M$, define the internal constructible hierarchy by the usual recursion:
\begin{align*}
L^M_0 &= \varnothing, \\
L^M_{\alpha+1} &= \operatorname{Def}^M(L^M_\alpha), \\
L^M_\lambda &= \bigcup_{\alpha \in \lambda} L^M_\alpha \quad \text{for limit ordinals } \lambda \text{ of } M,
\end{align*}
where $\operatorname{Def}^M(L^M_\alpha)$ denotes the subsets of $L^M_\alpha$ that are first-order definable over the structure $(L^M_\alpha,\in)$ using parameters from $L^M_\alpha$, as computed in $M$. Let
\begin{align*}
L^M := \bigcup_{\alpha \in \operatorname{Ord}^M} L^M_\alpha,
\end{align*}
where $\operatorname{Ord}^M$ is the class of ordinals of $M$.
By the theorem that the constructible universe of a model of $\mathsf{ZFC}$ is an inner model of $\mathsf{ZFC}$, the structure $L^M$ satisfies
\begin{align*}
L^M \models \mathsf{ZFC}.
\end{align*}
(citing a result not yet in the wiki: The Constructible Universe Is an Inner Model of $\mathsf{ZFC}$)
[guided]
The purpose of this step is to replace the arbitrary model $M$ by its constructible part. We define the internal hierarchy exactly as $M$ defines it:
\begin{align*}
L^M_0 &= \varnothing, \\
L^M_{\alpha+1} &= \operatorname{Def}^M(L^M_\alpha), \\
L^M_\lambda &= \bigcup_{\alpha \in \lambda} L^M_\alpha \quad \text{for limit ordinals } \lambda \text{ of } M.
\end{align*}
Here $\operatorname{Def}^M(L^M_\alpha)$ means the subsets of $L^M_\alpha$ that are definable over $(L^M_\alpha,\in)$ by first-order formulas, allowing parameters from $L^M_\alpha$, with definability interpreted inside $M$.
Now collect all stages indexed by the ordinals of $M$:
\begin{align*}
L^M := \bigcup_{\alpha \in \operatorname{Ord}^M} L^M_\alpha.
\end{align*}
The previously established inner-model theorem for constructibility applies because $M \models \mathsf{ZFC}$. Its conclusion is that $L^M$, with the inherited membership relation, is a model of every axiom of $\mathsf{ZFC}$:
\begin{align*}
L^M \models \mathsf{ZFC}.
\end{align*}
(citing a result not yet in the wiki: The Constructible Universe Is an Inner Model of $\mathsf{ZFC}$)
[/guided]
[/step]
[step:Verify that the internal constructible universe satisfies $V=L$]
By the theorem that the constructible universe satisfies constructibility, every set of $L^M$ appears at some stage of the constructible hierarchy computed in $L^M$. Hence
\begin{align*}
L^M \models V=L.
\end{align*}
(citing a result not yet in the wiki: The Constructible Universe Satisfies $V=L$)
[guided]
We must check not only that $L^M$ satisfies the axioms of $\mathsf{ZFC}$, but also that it satisfies the additional axiom $V=L$. The relevant constructibility theorem says that when the constructible universe is viewed as a universe in its own right, every one of its sets is constructible in that universe.
Applied to the structure $L^M$, this gives
\begin{align*}
L^M \models V=L.
\end{align*}
Thus $L^M$ is not merely a model of $\mathsf{ZFC}$; it is a model of the strengthened theory $\mathsf{ZFC}+V=L$.
(citing a result not yet in the wiki: The Constructible Universe Satisfies $V=L$)
[/guided]
[/step]
[step:Conclude consistency of $\mathsf{ZFC}+V=L$ from the existence of $L^M$]
Combining the previous two steps,
\begin{align*}
L^M \models \mathsf{ZFC}+V=L.
\end{align*}
Therefore the theory $\mathsf{ZFC}+V=L$ has a model. By soundness of first-order logic, every sentence derivable from a theory is true in every model of that theory. If $\mathsf{ZFC}+V=L$ proved a contradiction, then that contradiction would be true in $L^M$, impossible for a first-order structure. Hence $\mathsf{ZFC}+V=L$ is syntactically consistent.
This proves
\begin{align*}
\operatorname{Con}(\mathsf{ZFC}) \implies \operatorname{Con}(\mathsf{ZFC}+V=L).
\end{align*}
(citing a result not yet in the wiki: Soundness Theorem for First-Order Logic)
[/step]
