Where is "Well" needed in the Transfinite Recursion Theorem? The transfinite recursion theorem asserts
Let $R$ be a well-founded relation on $U$ and let $\digamma$ be a $R$-recursive rule on $U$. There is a unique function $f$ such that $\operatorname{dom}(f)=U$ and $f(x)=\digamma\left(x,f\restriction R^{-}[x]\right)$ for every $x\in U$.
I have a proof which is the standard one based on setting $f=\bigcup H$ where $h\in H$ iff $h$ is a function, and $\operatorname{dom}(h)$ is $R$-transitive in $U$, and $h(x)=\digamma\left(x,h\restriction R^{-}[x]\right)$ for every $x\in \operatorname{dom}(h)$.
I can't see where "wellness" comes into the proof, by which I mean I don't seem to need that $R^{-}[x]=\left\{ z\in U\mid z\mathbin Rx\right\}$ is a set for every $x$. I am using MK class theory not ZFC.
Can someone comment on the role of "wellness" in the proof in ZFC and whether it is still needed in the corresponding MK proof?
 A: The condition for $R$ being well-founded is not that $R^-[x]$ is always a set (if that was all, every relation on a set would be well-founded), but that every non-empty subset of $U$ has an $R$-minimal element.
As an example of a relation that doesn't have this property, consider the usual ordering $<$ on the closed unit interval $[0,1]$. The recursion theorem would fail for this set -- for example, consider
$$ \digamma(x,h) = \begin{cases} 0 & \text{if }[0,1]\cap\operatorname{Rng}h=\varnothing \\
\sup ([0,1]\cap \operatorname{Rng} h) & \text{otherwise} \end{cases} $$
This ought to satisfy your concept of a "$<$-recursive rule" on $[0,1]$.
However, this rule does not give rise to a unique $f$ -- in fact, every continuous non-decreasing $f:[0,1]\to[0,1]$ with $f(0)=0$ will satisfy the condition
$$ f(x)=\digamma\left(x,f\restriction R^{-}[x]\right) $$
so the recursion rule did not succeed in picking out a particular one among them.

The proof goes wrong in this case because $\bigcup H$ is not necessarily a function. In order to prove that it is, one needs the "well-founded" condition on $R$.
A: I am going to answer my own question. I had a lot of trouble finding
a simple proof of the recursion theorem online in the form I wanted, so will
post the one I eventually have put together. I am using MK class theory although that shouldn't be too relevant. Hopefully it is all correct, please let me know if there are errors. 
Let $R$ be a relation on class $U$. Recall that $R$ is founded
on $U$ if every $X\subseteq U\setminus\left\{ \varnothing\right\} $
has an $m\in X$ such that $X\cap R^{-}\left[m\right]=\varnothing$,
we call any such $m$ an $R$-first member of $X$. We say $R$ is
well-founded on $U$ if it is founded on $U$ and $R^{-}\left[x\right]:=\left\{ z\mid zRx\right\} $
is a set for every $x\in U$.
Given any $X\subseteq U$ we say $X$ is $R$-inductive on $U$ iff
for any $x\subseteq U$, if $R^{-}\left[x\right]\subseteq X$ then
$x\in X$.
Transfinite Induction Theorem: Let $R$ be a founded relation on $U$
and $X\subseteq U$. If $X$ is $R$-inductive in $U$ then $X=U$.
Proof: Suppose for contradiction that $X\subset U$ then $U\setminus X\neq\varnothing$
and so there is an $m\in U\setminus X$ such that $x\notin R^{-}\left[m\right]$
for any $x\in U\setminus X$. If $x\in R^{-}\left[m\right]$ then
we must have $x\in X$, otherwise we would have $x\in U\setminus X$
contrary to the selection of $m$ using foundedness, so $R^{-}\left[m\right]\subseteq X$
but $X$ is $R$-inductive so $m\in X$ contrary to $m\in U\setminus X$,
absurd. Hence $X\subseteq U$ but $X\not\subset U$ so $X=U$.$\square$
We say $\digamma$ is a $R$-recursive rule on $U$ if it is a function
and $\left\langle x,f\right\rangle \in\text{dom}\digamma$ whenever
$x\in U$ and $f$ is a function with $R^{-}\left[x\right]\subseteq\text{dom}f$.
Hence being a rule is a constraint on the domain of $\digamma$. We
require $f$ to be set so that $\left\langle x,f\right\rangle \in\text{dom}\digamma$
makes sense.
Transfinite Recursion Theorem: Let $R$ be a well-founded relation
on $U$ and let $\digamma$ be a $R$-recursive rule on $U$, There
is a unique function $f$ such that $\text{dom}f=U$ and $f\left(x\right)=\digamma\left(x,f\restriction R^{-}\left[x\right]\right)$
for every $x\in U$.$\square$
We will prove the recursion theorem by a sequence
of definitions and lemmas. 
We say $T$ is $R$-transitive in $U$ iff $T\subseteq U$ and $R^{-}\left[x\right]\subseteq T$
whenever $x\in T$. Clearly $U$ and $\varnothing$ are $R$-transitive
in $U$ and the $R$-transitive subclasses of $U$ are closed under
arbitrary intersections and unions.
Lemma: For every $A\subseteq U$ there is a smallest $R$-transitive
class $T$ such that $A\subseteq T$.
Proof: Set $T:=\bigcap\left\{ S\subseteq U\mid A\subseteq S\text{ and }S\text{ is }R\text{-transitive}\right\} $,
this definition works because $U$ is $R$-transitive by closure under
arbitrary intersections.$\square$
Next is the key lemma which is used several times in the following
proofs.
Lemma: Suppose $g,h$ are functions whose domains are $R$-transitive
in $U$ and are such that $g\left(x\right)=\digamma\left(x,g\restriction R^{-}\left[x\right]\right)$
and $h\left(x\right)=\digamma\left(x,h\restriction R^{-}\left[x\right]\right)$
for every $x$ in their respective domains, then $g=h$ on $\text{dom}g\cap\text{dom}h$.
Proof: First note that for any $x\in\text{dom}g\cap\text{dom}h$ we
have $R^{-}\left[x\right]\subseteq\text{dom}g\cap\text{dom}h$ 
 by $R$-transitivity, so $g\restriction R^{-}\left[x\right]$ and
$h\restriction R^{-}\left[x\right]$ are sets by well-foundedness
and so can participate in the domain of $\digamma$. 
Let $S:=\left\{ x\in\text{dom}g\cap\text{dom}h\mid g\left(x\right)\neq h\left(x\right)\right\} $.
Suppose for contradiction that $S\neq\varnothing$ and let $m$ be
an $R$-first member of $S$. Since $m\in\text{dom}g\cap\text{dom}h$
we have $R^{-}\left[m\right]\subseteq\text{dom}g\cap\text{dom}h$
by $R$-transitivity, and for any $x\in R^{-}\left[m\right]$ we have
$g\left(x\right)=h\left(x\right)$, otherwise $x$ would contradict
$m$ being $R$-first in $S$, so we have $g\restriction R^{-}\left[m\right]=h\restriction R^{-}\left[m\right]$.
Hence we have $g\left(m\right)=\digamma\left(m,g\restriction R^{-}\left[m\right]\right)=\digamma\left(m,h\restriction R^{-}\left[m\right]\right)=h\left(m\right)$,
absurd, so $S=\varnothing$ and $g=h$ on $\text{dom}g\cap\text{dom}h$.
$\square$
Lemma: Define $f$ by $\left\langle x,y\right\rangle \in f$ iff there
is a function $h$ such that $\left\langle x,y\right\rangle \in h$,
$\text{dom}h$ is $R$-transitive in $U$, and $h\left(x\right)=\digamma\left(x,h\restriction R^{-}\left[x\right]\right)$
for every $x\in\text{dom}h$. Then $f$ is the unique function such
that $\text{dom}f=U$ and is $R$-transitive, and $f\left(x\right)=\digamma\left(x,f\restriction R^{-}\left[x\right]\right)$
for every $x\in\text{dom}f$. 
Proof: For this proof call $h$ a recursor iff $h$ is a function
such that $\text{dom}h$ is $R$-transitive in $U$, and $h\left(x\right)=\digamma\left(x,h\restriction R^{-}\left[x\right]\right)$
for every $x\in\text{dom}h$. Note that if $\left\langle x,y\right\rangle \in f$
iff there is a recursor $h$ such that $x\in\text{dom}h$ and $h\left(x\right)=y$.
Consequently if $h$ is a recursor then $h\subseteq f$.
Since $f$ is a set of ordered pairs it is a relation. 
Suppose for contradiction that $f$ is not a function and let $m$
be an $R$-first member of $\text{dom}f$ at which $f$ is not single-valued.
Let $z_{1},z_{2}$ be two distinct values of $f$ at $m$ so $mfz_{1}$,
$mfz_{2}$ and $z_{1}\neq z_{2}$, so by definition there are recursors
$h_{1},h_{2}$ such that $mh_{1}z_{1}$ and $mh_{2}z_{2}$. By the
lemma we have $h_{1}=h_{2}$ on $\text{dom}h_{1}\cap\text{dom}h_{2}$
and since $m\in\text{dom}h_{1}\cap\text{dom}h_{2}$ we have $R^{-}\left[m\right]\subseteq\text{dom}h_{1}\cap\text{dom}h_{2}$
by $R$-transitivity, so $h_{1}=h_{2}$ on $R^{-}\left[m\right]$
so $z_{1}=h_{1}\left(m\right)=\digamma\left(m,h_{1}\restriction R^{-}\left[m\right]\right)=\digamma\left(m,h_{2}\restriction R^{-}\left[m\right]\right)=h_{2}\left(m\right)=z_{2}$,
absurd. Hence $f$ is a function.
If $x\in\text{dom}f$ and $z\in R^{-}\left[x\right]$, then $\left\langle x,f\left(x\right)\right\rangle \in f$
so there is a recursor $h$ such that $x\in\text{dom}h$ and $h\left(x\right)=f\left(x\right)$,
but $\text{dom}h$ is $R$-transitive so $z\in\text{dom}h$ and $h\left(z\right)=\digamma\left(z,h\restriction R^{-}\left[z\right]\right)$,
so by definition $\left\langle z,h\left(z\right)\right\rangle \in f$
so $z\in\text{dom}f$. Hence $R^{-}\left[x\right]\subseteq\text{dom}f$
so $\text{dom}f$ is $R$-transitive.
Let $x\in\text{dom}f$ be arbitrary then $\left\langle x,f\left(x\right)\right\rangle \in f$
so for some recursor $h$ we have $x\in\text{dom}h$ and $h\left(x\right)=f\left(x\right)=\digamma\left(x,h\restriction R^{-}\left[x\right]\right)$.
Since $x\in\text{dom}h\cap\text{dom}f$ we have $R^{-}\left[x\right]\subseteq\text{dom}h\cap\text{dom}f$
by $R$-transitivity and since $h\subseteq f$ we have $h\restriction R^{-}\left[x\right]=f\restriction R^{-}\left[x\right]$
so $f\left(x\right)=h\left(x\right)=\digamma\left(x,h\restriction R^{-}\left[x\right]\right)=\digamma\left(x,f\restriction R^{-}\left[x\right]\right)$. 
Suppose for contradiction that $\text{dom}f\subset U$ and let $m$
be an $R$-first member of $U\setminus\text{dom}f$. Let $f^{+}=f\cup\left\{ \left\langle m,\digamma\left(m,f\restriction R^{-}\left[m\right]\right)\right\rangle \right\} $
then since $m\notin\text{dom}f$ we have $f\subset f^{+}$. If $x\in\text{dom}f^{+}$
then either (1) $x\in\text{dom}f$ so $R^{-}\left[x\right]\subseteq\text{dom}f\subseteq\text{dom}f^{+}$
by $R$-transitivity, or (2) $x=m$ so any $z\in R^{-}\left[m\right]$
is in $\text{dom}f$ as $m$ is $R$-first, so $R^{-}\left[m\right]\subseteq\text{dom}f\subseteq\text{dom}f^{+}$,
hence in either case $R^{-}\left[x\right]\subseteq\text{dom}f^{+}$
so $\text{dom}f^{+}$ is $R$-transitive. Therefore $f^{+}$ is cleary
a recursor, $m\in\text{dom}f^{+}$ and $f^{+}\left(m\right)=\digamma\left(m,f\restriction R^{-}\left[m\right]\right)$
so $\left\langle m,\digamma\left(m,f\restriction R^{-}\left[m\right]\right)\right\rangle \in f$
so , absurd, so $\text{dom}f=U$.
Assume $g$ is also a function such that $\text{dom}g=U$ and $g\left(x\right)=\digamma\left(x,g\restriction R^{-}\left[x\right]\right)$
for every $x\in\text{dom}g$. Since $\text{dom}g=U$ it is $R$-transitive
so $g$ is a recursor so $g\subseteq f$. Suppose for contradiction
that $g\subset f$ then $\text{dom}g\subset\text{dom}f=U$, absurd.
Hence $g=f$.$\square$
