[proofplan] We first prove the set-sized recursion statement on each fixed ordinal $\theta$: there is a unique set function on $\theta$ satisfying the same recursive rule at every stage below $\theta$. The main point is compatibility: two correct initial approximations cannot first disagree, because the value at the first possible disagreement is determined by the common restriction below it. We then define the class function $F$ by taking, for each ordinal $\alpha$, the value assigned at $\alpha$ by the unique approximation on $\alpha + 1$. Compatibility of the set approximations gives the recursion equation and uniqueness of the resulting class function. [/proofplan] [step:Construct unique recursive approximations on each set ordinal] Fix an ordinal $\theta$. A $\theta$-approximation means a set function $h$ such that $\operatorname{dom}(h)$ is an ordinal $\gamma \subseteq \theta$ and, for every $\beta \in \gamma$, \begin{align*} h(\beta) = G(h|_\beta). \end{align*} Here $\gamma \subseteq \theta$ is ordinal inclusion; equivalently, every element of $\gamma$ is an element of $\theta$, and if $\gamma \neq \theta$ then $\gamma \in \theta$. The empty function is a $\theta$-approximation, so the class of $\theta$-approximations is nonempty. We first prove that any two $\theta$-approximations agree on their common domain. Let $h$ and $k$ be $\theta$-approximations, with domains $\gamma$ and $\delta$. Suppose that $h|_{\gamma \cap \delta} \neq k|_{\gamma \cap \delta}$. Since $\gamma \cap \delta$ is an ordinal, there is a least ordinal $\beta \in \gamma \cap \delta$ such that $h(\beta) \neq k(\beta)$. For every $\xi \in \beta$, minimality gives $h(\xi) = k(\xi)$, hence \begin{align*} h|_\beta = k|_\beta. \end{align*} Because $h$ and $k$ both satisfy the recursive rule, \begin{align*} h(\beta) = G(h|_\beta) = G(k|_\beta) = k(\beta), \end{align*} contradicting the choice of $\beta$. Therefore any two $\theta$-approximations agree on their common domain. We now form the maximal compatible approximation as a set, rather than taking an unrestricted class union. Define the set \begin{align*} D_\theta := \{\beta \in \theta : \text{there is a $\theta$-approximation $h$ with $\beta \in \operatorname{dom}(h)$}\}. \end{align*} This is a set by Separation from the set $\theta$. For each $\beta \in D_\theta$, compatibility gives a unique set $y$ such that $h(\beta)=y$ for some $\theta$-approximation $h$ with $\beta \in \operatorname{dom}(h)$. By the Axiom Schema of Replacement applied to the functional class relation just described, the graph \begin{align*} A_\theta := \{(\beta,y) : \beta \in D_\theta \text{ and } y=h(\beta) \text{ for some $\theta$-approximation $h$ with $\beta \in \operatorname{dom}(h)$}\} \end{align*} is a set. The same uniqueness shows that $A_\theta$ is a set function with domain $D_\theta$. The domain $D_\theta$ is an ordinal. Indeed, if $\beta \in D_\theta$ and $\xi \in \beta$, choose a $\theta$-approximation $h$ with $\beta \in \operatorname{dom}(h)$. Since $\operatorname{dom}(h)$ is an ordinal and $\xi \in \beta \in \operatorname{dom}(h)$, we have $\xi \in \operatorname{dom}(h)$, hence $\xi \in D_\theta$. Thus $D_\theta$ is transitive; as a transitive subset of the ordinal $\theta$, it is an ordinal. Write $\lambda := D_\theta$, so $\lambda \subseteq \theta$. Moreover, for every $\beta \in \lambda$, choosing a $\theta$-approximation $h$ with $\beta \in \operatorname{dom}(h)$ gives \begin{align*} A_\theta|_\beta = h|_\beta \end{align*} by compatibility, and hence \begin{align*} A_\theta(\beta) = h(\beta) = G(h|_\beta) = G(A_\theta|_\beta). \end{align*} Thus $A_\theta$ is itself a $\theta$-approximation. If $\lambda \neq \theta$, then $\lambda \in \theta$. Define a set function $A_\theta^+$ with domain $\lambda + 1$ by \begin{align*} A_\theta^+|_\lambda &= A_\theta, \\ A_\theta^+(\lambda) &= G(A_\theta). \end{align*} Then $A_\theta^+$ is a $\theta$-approximation strictly extending $A_\theta$. In particular, $\lambda \in \operatorname{dom}(A_\theta^+)$, so $\lambda \in D_\theta = \lambda$, contradicting the irreflexivity of ordinal membership. Hence $\lambda = \theta$. Therefore $A_\theta$ is a recursive set function on $\theta$. Uniqueness on $\theta$ follows from the same first-disagreement argument. If $h,k$ are set functions with domain $\theta$ satisfying the recursive rule and $h \neq k$, then the least $\beta \in \theta$ with $h(\beta) \neq k(\beta)$ satisfies $h|_\beta = k|_\beta$, so \begin{align*} h(\beta) = G(h|_\beta) = G(k|_\beta) = k(\beta), \end{align*} a contradiction. Thus the recursive set function on $\theta$ is unique. [/step] [step:Define the class function from the set approximations] For each ordinal $\theta$, let $F_\theta$ denote the unique set function with domain $\theta$ such that \begin{align*} F_\theta(\beta) = G(F_\theta|_\beta) \end{align*} for every $\beta \in \theta$. Define a class function \begin{align*} F: \mathrm{Ord} \to V \end{align*} by declaring that, for each ordinal $\alpha$, \begin{align*} F(\alpha) = F_{\alpha + 1}(\alpha). \end{align*} This is a class function because the defining condition “$y = F_{\alpha+1}(\alpha)$” is functional: the previous step gives a unique recursive set function on $\alpha+1$. We now verify compatibility of the approximations. If $\alpha \leq \theta$, then $F_\theta|_\alpha$ is a recursive set function on $\alpha$, since for every $\beta \in \alpha$, \begin{align*} (F_\theta|_\alpha)(\beta) = F_\theta(\beta) = G(F_\theta|_\beta) = G((F_\theta|_\alpha)|_\beta). \end{align*} By uniqueness of the recursive set function on $\alpha$, \begin{align*} F_\theta|_\alpha = F_\alpha. \end{align*} In particular, if $\beta < \alpha$, then applying this with $\theta = \alpha + 1$ gives \begin{align*} F(\beta) = F_{\beta+1}(\beta) = F_{\alpha+1}(\beta). \end{align*} Hence \begin{align*} F|_\alpha = F_{\alpha+1}|_\alpha. \end{align*} Using the recursive rule for $F_{\alpha+1}$ at the ordinal $\alpha$, we obtain \begin{align*} F(\alpha) = F_{\alpha+1}(\alpha) = G(F_{\alpha+1}|_\alpha) = G(F|_\alpha). \end{align*} Thus $F$ satisfies the desired recursion equation for every ordinal $\alpha$. [/step] [step:Prove uniqueness of the class solution] Let \begin{align*} H: \mathrm{Ord} \to V \end{align*} be any class function such that, for every ordinal $\alpha$, \begin{align*} H(\alpha) = G(H|_\alpha). \end{align*} We prove $H = F$. Suppose, toward a contradiction, that $H \neq F$. Then there is an ordinal $\alpha$ such that $H(\alpha) \neq F(\alpha)$. Let $\alpha$ be the least such ordinal. For every $\beta < \alpha$, minimality gives $H(\beta) = F(\beta)$, so the restrictions agree: \begin{align*} H|_\alpha = F|_\alpha. \end{align*} Applying the recursive rule for $H$ and for $F$ at $\alpha$ gives \begin{align*} H(\alpha) = G(H|_\alpha) = G(F|_\alpha) = F(\alpha), \end{align*} contradicting the choice of $\alpha$. Therefore no such ordinal exists, and $H = F$. This proves both existence and uniqueness of the class function satisfying the transfinite recursion equation. [/step]