Mostowski collapse lemma

The Mostowski collapse lemma states that every well-founded extensional relation on a set is isomorphic to membership on a unique transitive set.

Well-founded relation: A relation is well-founded when every nonempty subset of its domain has a minimal element. Well-foundedness makes the recursive definition of the collapse map terminate.
Binary relation: A binary relation on a set is a collection of ordered pairs drawn from that set. The lemma begins with an arbitrary relation on a set, not necessarily membership.
Axiom of Constructibility: The Axiom of Constructibility asserts that every set belongs to Gödel's constructible universe. Collapsing well-founded structures helps represent levels and models built inside constructible set theory.
Andrzej Mostowski: Andrzej Mostowski was a Polish logician and mathematician whose work included foundational set theory. The collapse lemma bears his name and is associated with his work on set-theoretic structures.
Extensional relation: A relation is extensional when distinct elements have distinct sets of predecessors. Extensionality ensures the collapse map distinguishes elements rather than identifying them.
Set: A set is a collection of distinct objects treated as a single mathematical object. The relation's domain must be a set for the lemma's stated form.
Countable transitive model: A countable transitive model is a countable set that is transitive and satisfies specified set-theoretic axioms. Collapsing a countable well-founded extensional model can produce a transitive model.
Set theory: Set theory is the mathematical study of sets, membership, and structures built from sets. The lemma is a standard tool for translating relational structures into set-theoretic membership.
Transitive set: A set is transitive when every element of one of its members is also one of its members. The collapse map's image is transitive under membership.
Axiom of Foundation: The Axiom of Foundation states that every nonempty set has a member disjoint from it. Foundation makes the membership relation well-founded in standard set theory.

Linked from 1 page

Axiom schema of replacementBroader topic: Its recursive construction uses replacement to collect the values assigned throughout the relation.