[proofplan] We construct the collapsing map $f$ by recursion on the well-founded relation $r$ via the formula $f(x) = \{f(y) : y \mathrel{r} x\}$. Well-foundedness of $r$ and locality (automatic because $r$ is a relation on a set) allow us to apply the $R$-Recursion Theorem. The image $b := f(a)$ is automatically transitive, and surjectivity is immediate. Injectivity uses **extensionality** of $r$: two elements with the same set of $r$-predecessors must be equal, which is exactly what the recursion equation translates via $f$ into the Axiom of Extensionality on $b$. The preservation property $x \mathrel{r} y \iff f(x) \in f(y)$ follows from the recursive definition together with injectivity. Uniqueness is a second $r$-induction. [/proofplan] [step:Define $f$ by $r$-recursion and verify the ambient hypotheses] Since $r$ is a relation on the set $a$, it is local: for every $x \in a$, $\{y \in a : y \mathrel{r} x\} \subseteq a$ is a set by Separation. Combined with well-foundedness of $r$, the [$R$-Induction and $R$-Recursion](/theorems/1496) theorem applies. Let $G$ be the function-class $G(h) := \operatorname{Range}(h)$, defined on all sets (here $\operatorname{Range}(h) = \{v : (u, v) \in h\}$). By $r$-recursion, there exists a unique function-class $F$ on all sets satisfying $F(x) = G(F|_{r,\, x}) = \operatorname{Range}(F|_{r,\, x}) = \{F(y) : y \mathrel{r} x\}$ for every set $x$. Let $f := F|_a$ be the restriction to the set $a$; by Replacement, $f$ is a set. The defining equation reads \begin{align*} f(x) = \{f(y) : y \mathrel{r} x\} \quad \text{for every } x \in a. \end{align*} Define $b := f(a) = \{f(x) : x \in a\}$, a set by Replacement. By construction $f : a \to b$ is surjective. [/step] [step:Verify that $b$ is transitive] Let $v \in u \in b$. By definition of $b$, there is some $x \in a$ with $u = f(x) = \{f(y) : y \mathrel{r} x\}$. Then $v \in u$ means $v = f(y)$ for some $y \mathrel{r} x$. In particular $y \in a$ (since $r$ is a relation on $a$), so $v = f(y) \in b$. Hence every member of a member of $b$ is itself a member of $b$, i.e., $b$ is transitive. [/step] [step:Prove $f$ is injective by $r$-induction using extensionality of $r$] [claim:Injectivity] For all $x, y \in a$, $f(x) = f(y) \implies x = y$. [/claim] [proof] We argue by $r$-induction on $x$. Let $\varphi(x)$ be the statement: *for every $y \in a$, $f(x) = f(y) \implies x = y$.* Fix $x \in a$ and assume $\varphi(z)$ holds for every $z \mathrel{r} x$ (the $r$-induction hypothesis). We prove $\varphi(x)$. Let $y \in a$ with $f(x) = f(y)$. By the recursive definition, \begin{align*} \{f(t) : t \mathrel{r} x\} = f(x) = f(y) = \{f(s) : s \mathrel{r} y\}. \end{align*} We show this forces $\{t \in a : t \mathrel{r} x\} = \{s \in a : s \mathrel{r} y\}$. *$\subseteq$ direction.* Fix $t \in a$ with $t \mathrel{r} x$. Then $f(t) \in \{f(t') : t' \mathrel{r} x\} = \{f(s) : s \mathrel{r} y\}$, so there is some $s \in a$ with $s \mathrel{r} y$ and $f(s) = f(t)$. Since $t \mathrel{r} x$, the inductive hypothesis $\varphi(t)$ applies: $f(s) = f(t)$ gives $s = t$. Hence $t = s \mathrel{r} y$, i.e., $t \mathrel{r} y$. *$\supseteq$ direction.* Symmetric — fix $s \in a$ with $s \mathrel{r} y$; then $f(s) \in \{f(t) : t \mathrel{r} x\}$, so $f(s) = f(t_0)$ for some $t_0 \mathrel{r} x$, and the inductive hypothesis $\varphi(t_0)$ gives $t_0 = s$, so $s \mathrel{r} x$. Combining, $\{t \in a : t \mathrel{r} x\} = \{s \in a : s \mathrel{r} y\}$. By **extensionality of $r$** (every two elements of $a$ with the same $r$-predecessors are equal), $x = y$. This proves $\varphi(x)$ and closes the induction. $\square$ [/proof] [guided] Why does extensionality of $r$ correspond exactly to injectivity of the Mostowski collapse? Unpack what $f(x) = f(y)$ says via the recursion: the sets $\{f(t) : t \mathrel{r} x\}$ and $\{f(s) : s \mathrel{r} y\}$ are equal. If we already knew $f$ were injective, this set-equality would pull back to $\{t : t \mathrel{r} x\} = \{s : s \mathrel{r} y\}$, and extensionality of $r$ would give $x = y$. Circular! The inductive hypothesis is what breaks the circle: when we are proving $\varphi(x)$, we are allowed to assume $\varphi(t)$ for every $t \mathrel{r} x$, i.e., injectivity of $f$ on the $r$-predecessors of $x$. That is exactly the level of injectivity we need to pull back the set equality. So the argument has two ingredients working together: - **The induction hypothesis** provides injectivity on $r$-predecessors, which translates the equation $f(x) = f(y)$ at the level of images to an equation $\{t : t \mathrel{r} x\} = \{s : s \mathrel{r} y\}$ at the level of predecessors. - **Extensionality of $r$** translates equality of predecessor sets to equality of the elements themselves. Without extensionality, $r$ could collapse "too much" — two elements with the same $r$-predecessors but distinct — and $f$ would not be injective. Indeed, the converse also holds: a well-founded relation on $a$ admits a Mostowski collapse to a transitive set iff it is extensional. [/guided] [/step] [step:Verify the preservation property $x \mathrel{r} y \iff f(x) \in f(y)$] **($\Rightarrow$).** If $x \mathrel{r} y$, then directly from the recursion $f(y) = \{f(t) : t \mathrel{r} y\}$ we see $f(x) \in f(y)$. **($\Leftarrow$).** Suppose $f(x) \in f(y)$. By the recursion, $f(y) = \{f(t) : t \mathrel{r} y\}$, so $f(x) = f(t_0)$ for some $t_0 \in a$ with $t_0 \mathrel{r} y$. By the injectivity of $f$ (previous step), $x = t_0$, and therefore $x \mathrel{r} y$. Hence $f$ is a bijection $a \to b$ satisfying the biconditional. [/step] [step:Prove uniqueness of $(b, f)$] Suppose $(b, f)$ and $(b', f')$ both satisfy the conclusion: $b, b'$ are transitive sets, $f: a \to b$ and $f': a \to b'$ are bijections, and $x \mathrel{r} y \iff f(x) \in f(y) \iff f'(x) \in f'(y)$ for all $x, y \in a$. **$f$ and $f'$ agree.** We show $f(x) = f'(x)$ for all $x \in a$ by $r$-induction. Fix $x \in a$ and assume $f(t) = f'(t)$ for every $t \mathrel{r} x$. We prove $f(x) = f'(x)$ by showing they have the same elements (Axiom of Extensionality on the universe). *$f(x) \subseteq f'(x)$.* Let $v \in f(x)$. Since $b$ is transitive and $f(x) \in b$, $v \in b$, so $v = f(t)$ for some $t \in a$ (surjectivity of $f$). Then $f(t) = v \in f(x)$ gives $t \mathrel{r} x$ by the preservation property of $(b, f)$. By the inductive hypothesis, $f(t) = f'(t)$, and by the preservation property of $(b', f')$, $t \mathrel{r} x$ gives $f'(t) \in f'(x)$. Hence $v = f(t) = f'(t) \in f'(x)$. *$f'(x) \subseteq f(x)$.* Symmetric, interchanging $(b, f)$ and $(b', f')$. Thus $f(x) = f'(x)$ for every $x \in a$, so $f = f'$. **$b = b'$.** Both equal $f(a)$, hence are the same set. $\square$ [/step]