The Mostowski Collapse Theorem

This entry formalizes the Mostowski collapse theorem in Isabelle/ZF [3, 4]. For a set equipped with a well-founded extensional relation, the development defines the collapsing map by well-founded recursion, proves that its range is transitive, and shows that the map is an order isomorphism between the original relation and membership on the transitive range. The construction is also proved unique among maps satisfying the same recursive equation. The result is a standard bridge from abstract well-founded extensional structures to transitive membership structures, and complements the existing Isabelle/ZF and AFP developments on ordinals, cardinals, forcing, and transitive models [2, 1]. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle