[proofplan] We prove existence and uniqueness separately. The strategy is to define a set-sized **attempt** — a function $f$ with transitive domain satisfying the recursion $f(y) = G(f|_y)$ on its domain — and to show (i) any two attempts agree on the intersection of their domains, (ii) for every set $x$ there exists an attempt defined at $x$. The function-class $F$ is then specified by the class formula "$y$ is the value at $x$ of some attempt defined at $x$", and well-definedness follows from (i). The key technical point is that $F|_x = \{(y, F(y)) : y \in x\}$ is a **set** (not a proper class), which is exactly what the Axiom of Replacement guarantees and what makes the expression $G(F|_x)$ meaningful. [/proofplan]

[step:Verify that $F|_x$ is a set so that $G(F|_x)$ is meaningful] Fix a set $x$. The expression $F|_x := \{(y, F(y)) : y \in x\}$ is the image of $x$ under the function-class $y \mapsto (y, F(y))$. Since $x$ is a set and the assignment is a definable function-class, the Axiom of Replacement produces a set \begin{align*} F|_x = \{(y, F(y)) : y \in x\}. \end{align*} Because $G$ is a function-class defined on **all sets**, $G(F|_x)$ is a well-defined term. This justifies writing the recursion equation $F(x) = G(F|_x)$ without a class/set type error. [/step]

[step:Define an attempt and prove two attempts agree wherever both are defined] Call a function $f$ an **attempt** if its domain $\operatorname{dom} f$ is a transitive set and $f(y) = G(f|_y)$ for every $y \in \operatorname{dom} f$. [claim:Agreement of attempts] If $f$ and $f'$ are attempts, then $f(y) = f'(y)$ for every $y \in \operatorname{dom} f \cap \operatorname{dom} f'$. [/claim] [proof] We argue by $\in$-induction on $y$. The $\in$-induction principle states: to prove $\forall y\, \varphi(y)$, it suffices to prove $(\forall z \in y\, \varphi(z)) \implies \varphi(y)$ for every set $y$. Let $\varphi(y)$ be the assertion: *if $y \in \operatorname{dom} f \cap \operatorname{dom} f'$, then $f(y) = f'(y)$*. Fix $y$ and assume $\varphi(z)$ holds for every $z \in y$. If $y \notin \operatorname{dom} f \cap \operatorname{dom} f'$ there is nothing to prove, so assume $y \in \operatorname{dom} f \cap \operatorname{dom} f'$. Since $\operatorname{dom} f$ and $\operatorname{dom} f'$ are transitive and $y \in \operatorname{dom} f \cap \operatorname{dom} f'$, every $z \in y$ lies in $\operatorname{dom} f \cap \operatorname{dom} f'$. By the induction hypothesis, $f(z) = f'(z)$ for every $z \in y$. Hence \begin{align*} f|_y = \{(z, f(z)) : z \in y\} = \{(z, f'(z)) : z \in y\} = f'|_y, \end{align*} and therefore \begin{align*} f(y) = G(f|_y) = G(f'|_y) = f'(y). \end{align*} This closes the induction. $\square$ [/proof] [/step]

[step:Construct an attempt defined at each set $x$ by $\in$-induction][claim:Existence of attempts] For every set $x$, there exists an attempt $f$ with $x \in \operatorname{dom} f$. [/claim] [proof] We argue by $\in$-induction on $x$. Fix $x$ and assume that for every $y \in x$ there exists an attempt $f_y$ with $y \in \operatorname{dom} f_y$. **Uniqueness of values at each $y \in x$.** By the agreement claim, the value $f_y(y)$ does not depend on the choice of attempt $f_y$: any two attempts both containing $y$ in their domains agree at $y$. Hence the class-function assignment $y \mapsto f_y(y)$ is well-defined on $x$. **Assembling a single attempt.** By Replacement, the set \begin{align*} h := \{(y, f_y(y)) : y \in x\} \end{align*} is a function with $\operatorname{dom} h = x$. In general $x$ need not be transitive, so $h$ itself is not yet an attempt. We extend $h$ to a function on the transitive closure $TC(x)$ as follows. For each $y \in x$, let $g_y$ denote the restriction of $f_y$ to $TC(\{y\})$ (which is transitive by definition of transitive closure). The agreement claim applied to distinct indices $y, y' \in x$ shows that $g_y$ and $g_{y'}$ agree on $TC(\{y\}) \cap TC(\{y'\})$. Define \begin{align*} f := \bigcup_{y \in x} g_y. \end{align*} By Replacement and Union, $f$ is a set; by the agreement claim it is a function; and its domain is $\bigcup_{y \in x} TC(\{y\}) = TC(x)$, which is transitive. For every $z \in TC(x)$ there is some $y \in x$ with $z \in TC(\{y\}) \subseteq \operatorname{dom} f_y$, so \begin{align*} f(z) = g_y(z) = f_y(z) = G(f_y|_z) = G(f|_z), \end{align*} where the last equality uses the agreement claim to identify $f_y|_z$ with $f|_z$ (both are the restriction to $z$ of any attempt defined on $z$, and $z \subseteq TC(x)$ since $TC(x)$ is transitive). Thus $f$ is an attempt with $\operatorname{dom} f = TC(x)$. **Extending to include $x$.** Set \begin{align*} f' := f \cup \{(x, G(f|_x))\}. \end{align*} Then $\operatorname{dom} f' = TC(x) \cup \{x\}$, which is transitive because $x \subseteq TC(x)$. For every $y \in TC(x)$ we already have $f'(y) = f(y) = G(f|_y) = G(f'|_y)$, using that $f$ and $f'$ agree on $TC(x)$ and that $y \in TC(x)$ implies $y \subseteq TC(x)$ so $f|_y = f'|_y$. At $y = x$ we have $f'(x) = G(f|_x) = G(f'|_x)$ since $x \subseteq TC(x)$, so $f|_x = f'|_x$. Therefore $f'$ is an attempt and $x \in \operatorname{dom} f'$. $\square$ [/proof][/step]

[guided]We want to prove: for each set $x$, there is some attempt that "reaches" $x$. Why not just try to build one big function all at once? Because the recursion is non-local: $f(x)$ is defined in terms of $f$ on all of $x$, whose members might require $f$ defined on their members, and so on. The natural domain for an attempt through $x$ is therefore the **transitive closure** $TC(x) \cup \{x\}$. The argument is by $\in$-induction on $x$. Fix $x$ and assume the induction hypothesis: for every $y \in x$, there exists an attempt $f_y$ with $y \in \operatorname{dom} f_y$. **Step 1 — the values at the members of $x$ are already determined.** By the agreement claim (which we proved first, using only the transitive-domain property and the recursion equation), the value $f_y(y)$ is the same regardless of which attempt we pick. So the class assignment $y \mapsto f_y(y)$ depends only on $y$, not on the choice of $f_y$. Replacement applied to the set $x$ and this class-function yields the set \begin{align*} h := \{(y, f_y(y)) : y \in x\}. \end{align*} **Step 2 — glue the attempts on transitive closures.** The function $h$ is defined on $x$, but $x$ need not be transitive, so $h$ is not yet an attempt. The fix is to glue together the pieces of the various $f_y$ that live on transitive sets. For each $y \in x$, let \begin{align*} g_y := f_y\big|_{TC(\{y\})}. \end{align*} The set $TC(\{y\})$ is transitive (it is the smallest transitive set containing $y$), and $g_y$ is an attempt because its domain is transitive and the recursion equation is inherited from $f_y$. For any two indices $y, y' \in x$, the agreement claim gives $g_y = g_{y'}$ on $TC(\{y\}) \cap TC(\{y'\})$, so \begin{align*} f := \bigcup_{y \in x} g_y \end{align*} is a single function (well-definedness is exactly the agreement). Its domain is $\bigcup_{y \in x} TC(\{y\}) = TC(x)$, which is transitive, and the recursion equation holds at every $z \in TC(x)$ because $z \in TC(\{y\})$ for some $y$ and $f$ agrees with $f_y$ on $TC(\{y\})$. **Step 3 — extend to include $x$ itself.** Define \begin{align*} f' := f \cup \{(x, G(f|_x))\}. \end{align*} Why does this work? First, $f|_x = \{(y, f(y)) : y \in x\}$ is a set by Replacement, and $f(y) = f_y(y)$ is exactly the value $h(y)$, so $G(f|_x)$ is a legitimate value. Second, $\operatorname{dom} f' = TC(x) \cup \{x\}$ is transitive because $x \subseteq TC(x) \subseteq \operatorname{dom} f'$. Third, the recursion equation holds at $x$ because $f|_x = f'|_x$ (the members of $x$ lie in $TC(x)$, where $f$ and $f'$ agree), and at every $y \in TC(x)$ it holds because $f'$ agrees with $f$ there. This completes the induction: $f'$ is an attempt with $x \in \operatorname{dom} f'$, establishing the claim for this $x$.[/guided]

[step:Define the function-class $F$ and verify the recursion equation] Define the class-relation $q$ by \begin{align*} q(x, y) \iff \text{there exists an attempt } f \text{ with } x \in \operatorname{dom} f \text{ and } f(x) = y. \end{align*} **$q$ is a function-class.** The existence of attempts (previous step) shows that for every set $x$ there is some $y$ with $q(x, y)$. The agreement of attempts (first step) shows that $y$ is uniquely determined by $x$: if $q(x, y)$ and $q(x, y')$ via attempts $f, f'$, then $y = f(x) = f'(x) = y'$. Define the function-class $F$ by $F(x) := y$, where $y$ is the unique set with $q(x, y)$. **$F$ satisfies the recursion.** Fix a set $x$ and let $f'$ be an attempt with $x \in \operatorname{dom} f'$ (such an attempt exists by the previous step). For every $y \in x$ we have $y \in \operatorname{dom} f'$ by transitivity of $\operatorname{dom} f'$, so $F(y) = f'(y)$ by definition of $F$. Hence \begin{align*} F|_x = \{(y, F(y)) : y \in x\} = \{(y, f'(y)) : y \in x\} = f'|_x, \end{align*} and therefore \begin{align*} F(x) = f'(x) = G(f'|_x) = G(F|_x), \end{align*} where the middle equality uses that $f'$ is an attempt. [/step]

[step:Prove uniqueness of $F$] Suppose $F_1$ and $F_2$ are both function-classes satisfying $F_i(x) = G(F_i|_x)$ for every set $x$. We show $F_1(x) = F_2(x)$ by $\in$-induction. Fix $x$ and assume $F_1(y) = F_2(y)$ for every $y \in x$. Then \begin{align*} F_1|_x = \{(y, F_1(y)) : y \in x\} = \{(y, F_2(y)) : y \in x\} = F_2|_x, \end{align*} so \begin{align*} F_1(x) = G(F_1|_x) = G(F_2|_x) = F_2(x). \end{align*} By $\in$-induction, $F_1 = F_2$ as function-classes. This completes the proof. $\square$ [/step]