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)...