Solution (source code)

= Solution

\b[The rank characterization holds for a set relation, or a <set-like> class relation.] For such a <well-founded relation>, use <well-founded recursion> to define
$$
\boxed{\rho(y)=\sup\{\rho(x)+1:xRy\}.}
$$
The predecessor set is a set, so the <supremum> is an <ordinal>. For a <set-like> class relation, the closure of the predecessors of any one point under finitely many predecessor steps is a set; perform the ordinary set recursion there. Uniqueness makes these local definitions agree, producing a class rank function. The formula immediately gives $xRy\Rightarrow\rho(x)<\rho(y)$.

Conversely, suppose such an ordinal-valued function exists. For any nonempty subset, or nonempty subclass in the class formulation, take an element whose rank is least among the ranks occurring. It has no predecessor in that subset or subclass, because a predecessor would have smaller rank. This proves well-foundedness.

There is a qualification in the printed class formulation. If well-founded class relations are defined to include <set-likeness>, it is already implicit and the assertion is correct. Under the minimal-element definition alone, it must be supplied. Without <set-likeness>, let $X=\operatorname{Ord}\cup\{u\}$, where $u=\{1\}$ is not an <ordinal>, and put every ordinal below $u$, with the usual ordinal order below it. Every nonempty subclass has a minimal element, so the relation is well founded. But <transfinite induction> forces $\rho(\alpha)\geq\alpha$ for all ordinals, whereas $\rho(u)$ would have to exceed every $\rho(\alpha)$. No such ordinal exists. Thus the unrestricted class assertion is false; \b[set-likeness is necessary for this standard rank proof].