= Solution
Read epsilon as actual set membership restricted to $X$, the interpretation in which ambient ZF makes the relation <well-founded>. The structure's <axiom of extensionality> assumption means
$$
x,x'\in X,\quad x\cap X=x'\cap X\quad\Longrightarrow\quad x=x'.
$$
By <well-founded recursion> on membership, define
$$
\boxed{\pi(x)=\{\pi(y):y\in x\cap X\}\qquad(x\in X).}
$$
The recursion theorem applies because the <Axiom of foundation> makes the restricted relation <well-founded> and each predecessor collection is a set. The <Axiom schema of replacement> gives the set $M=\pi[X]$.
To prove injectivity, use membership induction on $x$ for the property that $x\in X$ and $\pi(x)=\pi(x')$ with $x'\in X$ imply $x=x'$. Suppose this property holds for every $y\in x\cap X$. Equality of the two images means that each $y\in x\cap X$ has some $y'\in x'\cap X$ with $\pi(y)=\pi(y')$, so the induction hypothesis gives $y=y'$. Conversely every $y'\in x'\cap X$ has the same image as some $y\in x\cap X$, and the same induction hypothesis again makes them equal. Hence $x\cap X=x'\cap X$, and the structure's <axiom of extensionality> gives $x=x'$.
The map is onto $M$ by definition. The recursion immediately preserves membership, and its injectivity makes membership reflection valid as well. Moreover if $z\in\pi(x)$ then $z=\pi(y)$ for a predecessor $y\in X$, so $z\in M$. Therefore $M$ is transitive and $\pi$ is the required membership isomorphism. This proves the existence direction of the <Mostowski collapse theorem>.
\b[An arbitrary binary relation must also be <well-founded>.] <Axiom of extensionality> alone is insufficient in that interpretation: the one-element relation with a self-loop is extensional, but any collapse onto a <transitive set> would produce a set containing itself, contrary to <Axiom of foundation>. The actual-membership interpretation above supplies precisely the hypothesis otherwise missing; no analogous claim is made for a general ill-founded relation.
Back to article page
