The Mostowski collapse theorem applies when is a well-founded relation and an extensional relation on the set . Extensionality here means that different points have different sets of -predecessors. There is then a unique transitive set and a unique bijection such that
The collapsing map is characterized by well-founded relation recursion:
Thus is isomorphic to . Both well-foundedness and extensionality are hypotheses of the theorem; well-foundedness alone does not make the recursive map injective.
The epsilon-recursion theorem says that for every definable operation assigning a set to each set and each function with domain , there is a unique class function such that
for every set .
For uniqueness, suppose and both satisfy the recursion. If they agree on every , then their restrictions to agree and hence
The epsilon induction principle therefore gives .
For existence, call a function coherent on a transitive set when
The same epsilon-induction argument shows that any two coherent functions agree on the intersection of their transitive domains. Assuming coherent functions have been constructed below every member of , their compatible union defines all values below ; adjoining the value prescribed by extends the construction to . Epsilon induction establishes this construction for every . The compatible local functions therefore unite to the required class function .
A relation on is well-founded when every nonempty subset of has an element with no -predecessor in that subset. It is extensional when
The Mostowski collapse theorem states that every well-founded extensional relation is isomorphic to membership on a unique transitive set . Define recursively
Well-founded recursion makes well defined. Epsilon-style induction along , together with extensionality, shows that is injective. By definition,
so is an isomorphism from onto , where . If , then for some , so ; hence is transitive. If another collapse has transitive range, induction gives , proving uniqueness.
Finally, suppose is finite. Its collapse is a finite transitive set, so every member of is hereditarily finite. Therefore every well-founded extensional relation on collapses to a transitive subset of .
Conversely, let be infinite. Choose the initial infinite ordinal equinumerous with . The successor ordinal has the same cardinality as . Pulling its membership relation back along a bijection gives a well-founded extensional relation on whose collapse is . But is not hereditarily finite, so . Consequently,
A relation on a set is well-founded when every nonempty subset of has an -minimal element. It is extensional when distinct elements have distinct predecessor sets:
The Mostowski collapse theorem states that every well-founded extensional relation on a set is uniquely isomorphic to membership on a transitive set; the collapse is recursively
For the requested example, let and define
No belongs to , and therefore
The map is an isomorphism from membership on to membership on the von Neumann ordinal , so the Mostowski collapse is . On the other hand, already has rank , and hence the rank of is greater than .
For statement (i), suppose is isomorphic to with transitive. Membership is well-founded by the axiom of foundation. It is extensional on because transitivity ensures that the predecessors in of an element are exactly the elements of , and the axiom of extensionality distinguishes different sets. Both properties are preserved by isomorphism. Thus (i) is always true.
Write for the equivalence class of in the ultrapower
and define its membership relation by
The kappa-complete filter property makes well-founded: an infinite descending -chain would give countably many members of whose intersection belongs to , and every index in that intersection would yield an infinite descending membership chain, contradicting the Axiom of foundation. The relation is extensional by Łoś's theorem.
The Mostowski collapse theorem therefore gives a unique isomorphism onto a transitive set . Recursively, the notation missing from the printed formula may be defined by
The value is independent of the representative because it is defined on the ultrapower class . Moreover : every has its range contained in some with , since and the strongly inaccessible cardinal is regular; induction on the resulting rank bound keeps inside .
Define the ultrapower embedding
The constant-function map into is elementary by Łoś's theorem, and is an isomorphism, so their composite is elementary.