There are several formulations of transfinite recursion. I am interested in the following one.
Let $(V, \in)$ be a model of ZF. Let $g_1$ be a set and $G_2,G_3 : V \to V$ be two definable class functions. Then there is a unique definable class function $F : \text{Ord} \to V$ such that
$(1)$ $F(\emptyset) = g_1.$
$(2)$ $F(\alpha) = G_2(\beta,F(\beta))$ if $\alpha =\beta+1$ is a successor ordinal.
$(3)$ $F(\alpha) = G_3(F|_{\alpha})$ if $\alpha$ is a limit ordinal.
I can prove the uniqueness thanks to transfinite induction (which is also stated in three cases) but I have some trouble with the existence. How should I define $F$ as a class of couples ?
$$ \begin{align} F&=\{\langle \alpha, X\rangle : \text{Ordinal}(\alpha) \land \exists f\,(\text{Function}(f)\land\text{Domain}(f)=(\alpha+1)\\ &\land f(0)=g_1 \land \forall \beta\,(\beta + 1 \le \alpha \implies \exists Y,Z (Y=f(\beta)\land Z=G_2(\beta,Y)\land f(\beta+1) = Z))\\ &\land\forall \beta\,(\beta \le \alpha\land\beta\ne 0\land\text{LimitOrdinal}(\beta)\\ &\implies \exists Y,Z(Y=\text{Restriction}(f,\beta)\land Z=G_3(Y)\land f(\beta)=Z))\\ &\land f(\alpha)=X)\} \end{align} $$