Mostowski's Collapsing Theorem

Let be Well-Founded, Extensional relation on a set .
(Note that this implies is Local)
Then there is a Transitive set and a bijection
such that:

Moreover, the pair is unique.

Note

Similar to Epsilon-recursion Theorem and Principle of Epsilon-Induction
we can define the same concepts for (as well as -closure)

Proof

Define by -recursion

and set
Now verify the conditions.
Everything is straightforward except injective and unique
These we verify by induction.