Ordinal rank of a well-founded relation

For a well-founded setlike relation $R$ on $X$, its ordinal rank is the definable function determined by

${\rho }_R(x)=\sup \{{\rho }_R(y)+1:yRx\}=\bigcup \{{\rho }_R(y)\cup \{{\rho }_R(y)\}:yRx\}\mathrm{.}$

To justify the definition, apply well-founded recursion to the total rule which returns this union if every value of its input function is an ordinal and returns $0$ otherwise. Well-founded induction shows that every actual value is an ordinal: predecessor values are ordinals by the induction hypothesis, their successors are ordinals, Replacement collects them, and their union is an ordinal, including the empty union $0$. Thus the default case never occurs. For $yRx$ the rank equation gives ${\rho }_R(y)<{\rho }_R(x)$. The definition requires no ambient Foundation for a supplied well-founded $R$.

Conventions and prerequisites: Recursion on well-founded setlike relations, Basic closure properties of ordinals.