An extensional collapse is injective

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

A setlike relation $R$ on $X$ is extensional when ${\mathrm{pred}}_R(x)={\mathrm{pred}}_R(y)$ implies $x=y$ for $x,y\in X$. If $R$ is also well-founded, its collapse map is the unique definable function $\pi (x)=\{\pi (y):yRx\}\mathrm{.}$ Existence and uniqueness follow from well-founded recursion with $G(x,h)=\mathrm{ran}(h)$, a set by Replacement. A collapse map is defined even without extensionality; injectivity is a further conclusion requiring extensionality. The construction for a supplied well-founded relation uses no ambient Foundation. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations. (Extensional relations and collapse maps)

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: thm-recursion-on-well-founded-setlike-relations, lem-ordinal-basics. (Ordinal rank of a well-founded relation)