Cardinality of infinite constructible levels

The order from F2 restricts to a well-order of $L_{\alpha }$. F5 gives the injection $\alpha \hookrightarrow L_{\alpha }$ by inclusion. Thus both cardinals exist and $\mathrm{\mid }\alpha \mathrm{\mid }\le \mathrm{\mid }{L}_{\alpha }\mathrm{\mid }$.

Encode descriptions by finite rooted ordered trees. A node carries a label $(\gamma ,i)$ with $\gamma <\alpha$ and i the code of a formula defining a subset of $L_{\gamma }$; its ordered children describe the finite tuple of parameters. A valid tree evaluates its children first and then takes the subset defined by that formula over the indicated level. Empty-level descriptions use the prescribed $\mathrm{Def}(\mathrm{\varnothing })=\{\mathrm{\varnothing }\}$. Each valid tree has at most one value, by uniqueness of satisfaction and of its recursively evaluated parameters.

Every $x\in L_{\alpha }$ has a valid finite description. Induct on ${\rho }_L(x)$. Choose one definition of x over $L_{\gamma }$, where $\gamma ={\rho }_L(x)<\alpha$. Each parameter has smaller constructible rank by F1 and nesting. By the induction hypothesis it has a finite description; finitely many existential choices of descriptions are provable in ZF by induction on the tuple length. Joining those finitely many finite trees under the root $(\gamma ,i)$ gives a finite description of x. The zero-parameter case is a single node, covering the first stage. This induction proves existence, without choosing definitions simultaneously for all x.

Put $\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$. Fix one bijection $\alpha \to \kappa$ from F3 and one pairing bijection on $\kappa$ from F4. Encode node labels and finitely many punctuation symbols in $\kappa$. Iterating this fixed pairing and including the string length injects all finite strings, hence all the described finite trees, into $\kappa$. For a nonempty fibre of the tree-evaluation map take its least ordinal code. Step 1.2 ensures different values have disjoint fibres; step 2.1 ensures every x has a nonempty fibre. Least codes therefore give an injection $L_{\alpha }\to \kappa$.

The upper bound in step 3.1 and the lower bound in step 1.1 imply $\mathrm{\mid }{L}_{\alpha }\mathrm{\mid }=\mathrm{\mid }\alpha \mathrm{\mid }$. In particular at $\alpha =\omega$ the finite-tree codes are natural-number codes and the lower bound consists of the finite ordinals. The same code alphabet works at successor and limit ordinals alike; no family of levelwise bijections, and no AC, was used.