Confused by proof that $L$ is a model of $ZF$ in Jech's set theory

In Chapter 12 of Jech's Set Theory, the model $$L$$ is defined as:

\begin{align} L_0 & = \emptyset, L_{\alpha+1} = \text{def}(L_{\alpha}), \\ L_{\alpha} &= \bigcup_{\beta < \alpha} L_{\beta} \text{ for limit ordinal \alpha} \\ L &= \bigcup_{\alpha \in Ord} L_{\alpha} \end{align}

where $$\text{def}(M) = \{ X \subset M : X \text{ is definable over (M,E)} \}$$

He then proves in Theorem 13.3 that $$L$$ is a model of $$ZF$$. However, all the proofs for Theorem 13.3 that $$L$$ satisfies all the axioms of $$ZF$$ are based on the fact that $$L$$ is a transitive set ...

This is what I would like to clarify ... because I could not wrap my head around this chicken-and-egg situation, i.e., to prove that $$L$$ is a model of $$ZF$$, we can rely on the fact that $$L$$ is transitive and use the absolute formula theorem (i.e. any absolute formula of set theory in $$ZF$$ holds in any transitive model).

However, to prove that $$L$$ is transitive (and then make use of the absolute formula theorem), I think that I have to use set-theoretic operations on $$L_{\alpha}$$ for each $$\alpha$$ ... But these set-theoretic operations rely on $$ZF$$ axioms (i.e. pairing, separation, powerset, etc) which I would still have to prove are satisfied by $$L$$ ...

What am I missing here ? (or is it that the operations done on $$L$$, (i.e. in the model $$(L,\in)$$ are to be considered distinct from the set theory operations (in the meta language of set theory) they could be considered as doing basically the same thing)...

• You can use that the ZF axioms hold in $V$ (but need to prove they hold in $L$). The $L_\alpha$ are just sets in $V,$ so you can apply set theoretical operations on them in your attempt to prove that ZF holds in $L$. (As a simple example, if $x,y\in L$ you're free to form the pair $\{x,y\}$... the content of showing pairing holds in $L$ is just showing that $\{x,y\}\in L$ when $x,y \in L.$) It's hard to say more without knowing what precise steps you have doubts about. Mar 4 at 2:21
• The proof is a relative consistency proof. It assumes the axioms of ZF hold in the universe, then use them to prove each $L_\alpha$ is transitive, and $\bigcup_\alpha L_\alpha$ is transitive. You don't need $L$ to be a model of ZF for that. You need the universe to a model of ZF. There are transitive classes that are not models of ZF and can be proved to be transitive by applying ZF axioms in the universe. Mar 4 at 10:28