Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal

For every ordinal $\gamma$ the pair $(\gamma, \in)$ is a well-order, by clause 2 of the definition of an ordinal.

For $\beta \in \gamma$ the initial segment of $(\gamma, \in)$ determined by $\beta$ is $\gamma_{<\beta} = \{x \in \gamma : x \in \beta\} = \beta$, because $\beta \subseteq \gamma$ by transitivity of $\gamma$; so by [L3] the proper initial segments of $(\gamma, \in)$ are exactly the ordinals $\beta \in \gamma$, and a function whose domain is one of them is a function whose domain is an ordinal, to which $G$ applies.

If $\xi \in \beta$ then $\xi^{+} \in \beta^{+}$: transitivity of $\beta$ gives $\xi \subseteq \beta$, and $\xi \in \beta$ gives $\{\xi\} \subseteq \beta$, so $\xi^{+} \subseteq \beta$, whence $\xi^{+} \in \beta$ or $\xi^{+} = \beta$ by [L4], and either way $\xi^{+} \in \beta \cup \{\beta\} = \beta^{+}$.

Applying [L1] to the well-order $(\gamma, \in)$ and to $G$ yields, for each ordinal $\gamma$, exactly one function $F_\gamma$ with domain $\gamma$ satisfying $F_\gamma(\beta) = G(F_\gamma \restriction \beta)$ for every $\beta \in \gamma$.

Coherence: for $\delta \in \gamma$ put $u = F_\gamma \restriction \delta$, a function with domain $\delta$; for $\beta \in \delta$ transitivity of $\delta$ gives $\beta \subseteq \delta$, so $u \restriction \beta = F_\gamma \restriction \beta$ and $u(\beta) = F_\gamma(\beta) = G(F_\gamma \restriction \beta) = G(u \restriction \beta)$, so $u$ satisfies the recursion on $\delta$ and the uniqueness half of [L1] applied to $(\delta, \in)$ gives $F_\gamma \restriction \delta = F_\delta$.

Define $F(\beta) := F_{\beta^{+}}(\beta)$, which makes sense because $\beta^{+}$ is an ordinal by [L4] and $\beta \in \beta^{+}$; the defining condition is a formula in $\beta$, so $F$ is a class function defined at every ordinal.

For every ordinal $\beta$ and every $\xi \in \beta$ we have $\xi^{+} \in \beta^{+}$, hence $F_{\beta^{+}} \restriction \xi^{+} = F_{\xi^{+}}$ and therefore $F_{\beta^{+}}(\xi) = F_{\xi^{+}}(\xi) = F(\xi)$; so $F \restriction \beta = F_{\beta^{+}} \restriction \beta$, which is a set because $F_{\beta^{+}}$ is.

Consequently $F(\beta) = F_{\beta^{+}}(\beta) = G(F_{\beta^{+}} \restriction \beta) = G(F \restriction \beta)$ for every ordinal $\beta$, which is the required recursion equation.

For uniqueness, let $F'$ be a class function defined at every ordinal with $F'(\beta) = G(F' \restriction \beta)$ for every $\beta$, and suppose $F(\beta_0) \ne F'(\beta_0)$ for some ordinal $\beta_0$; then $D = \{\xi \in \beta_0^{+} : F(\xi) \ne F'(\xi)\}$ is a set by Separation, it is a set of ordinals by [L4], and it is nonempty because $\beta_0 \in D$, so it has an $\in$-least element $\mu$ by [L5].

Every $\xi \in \mu$ lies in $\beta_0^{+}$, because $\mu \in \beta_0^{+}$ gives $\mu \subseteq \beta_0^{+}$, and $\xi \notin D$ by minimality of $\mu$, so $F(\xi) = F'(\xi)$; hence $F \restriction \mu = F' \restriction \mu$ and $F(\mu) = G(F \restriction \mu) = G(F' \restriction \mu) = F'(\mu)$, contradicting $\mu \in D$.

No such $\beta_0$ exists, so $F$ and $F'$ agree at every ordinal, and $F$ is the unique class function on the ordinals satisfying $F(\beta) = G(F \restriction \beta)$.