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.