Solution (source code)

= Solution

The <Mostowski collapse theorem> states that if $R$ is a well-founded extensional relation on a set $X$, then there is a unique transitive set $M$ and a unique bijection $\pi:X\to M$ such that
$$
\boxed{xRy\quad\Longleftrightarrow\quad\pi(x)\in\pi(y).}
$$
Extensionality means that distinct elements of $X$ have distinct predecessor sets. The collapse is characterized by the recursion
$$
\pi(y)=\{\pi(x):xRy\}.
$$
Well-founded recursion defines it, extensionality makes it injective, and its range is transitive. Uniqueness follows by <well-founded induction>. For a class version, the relation must also be <set-like>; its predecessor sets must be sets.