The canonical definable global well-order of L

Recurse on ordinal intervals, keeping an order ${<}_{\alpha }$ on $L_{\alpha }$. At zero use the empty order. At $\alpha +1$ retain ${<}_{\alpha }$ on the old elements, put every old element before every member of $L_{\alpha +1}\setminus L_{\alpha }$, and order the new elements by their least Def codes over $(L_{\alpha },{<}_{\alpha })$ from F1. At nonzero limits take the union of earlier orders. On malformed histories one may return the empty relation, so the recursion rule is total and definable.

Induction proves these are coherent well-orders and each earlier level is an initial segment. The successor order is the sum of the old well-order and a subset of the code well-order. At a limit, comparisons of finitely many elements take place in a common earlier level, giving a total transitive strict order. For a nonempty subset S of the limit level, take any $x\in S$ in an earlier level; the least member of the nonempty intersection of S with that level is least in all of S, since the level is an initial segment. This single existential choice proves well-ordering without a choice function.

Interval uniqueness gives a uniform formula for all these orders. Their class union defines ${<}_L$ without set parameters. The same initial-segment argument as step 2.1 gives a least element to every nonempty set subset of L (and to any specified nonempty definable subclass, by Separation in a level). For $x\in L_{\alpha }$, every predecessor of x lies in $L_{\alpha }$, so Separation makes its predecessor collection a set.

Inside L the construction is licensed by the ZF axioms in F4–F7 and has exactly the same levels by F8. Induct on alpha to compare orders. At successors, F9 identifies internal and external Def on the old level. The previous order is identical, hence code comparison, decoding fibres and their least codes are identical. At limits the unions agree. Thus the two constructions produce the same restrictions and the same class relation.