Metamath Proof Explorer

Table of Contents - 2. ZF (ZERMELO-FRAENKEL) SET THEORY

Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets". A set can be an element of another set, and this relationship is indicated by the symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects.

A simplistic concept of sets, sometimes called "naive set theory", is vulnerable to a paradox called "Russell's Paradox" (ru), a discovery that revolutionized the foundations of mathematics and logic. Russell's Paradox spawned the development of set theories that countered the paradox, including the ZF set theory that is most widely used and is defined here.

Except for Extensionality, the axioms basically say, "given an arbitrary set x (and, in the cases of Replacement and Regularity, provided that an antecedent is satisfied), there exists another set y based on or constructed from it, with the stated properties". (The axiom of extensionality can also be restated this way as shown by axexte.) The individual axiom links provide more detailed descriptions. We derive the redundant ZF axioms of Separation, Null Set, and Pairing from the others as theorems.

1. ZF Set Theory - start with the Axiom of Extensionality
   1. Introduce the Axiom of Extensionality
   2. Classes
   3. Class form not-free predicate
   4. Negated equality and membership
   5. Restricted quantification
   6. The universal class
   7. Conditional equality (experimental)
   8. Russell's Paradox
   9. Proper substitution of classes for sets
   10. Proper substitution of classes for sets into classes
   11. Define basic set operations and relations
   12. Subclasses and subsets
   13. The difference, union, and intersection of two classes
   14. The empty set
   15. The conditional operator for classes
   16. The weak deduction theorem for set theory
   17. Power classes
   18. Unordered and ordered pairs
   19. The union of a class
   20. The intersection of a class
   21. Indexed union and intersection
   22. Disjointness
   23. Binary relations
   24. Ordered-pair class abstractions (class builders)
   25. Functions in maps-to notation
   26. Transitive classes
2. ZF Set Theory - add the Axiom of Replacement
   1. Introduce the Axiom of Replacement
   2. Derive the Axiom of Separation
   3. Derive the Null Set Axiom
   4. Theorems requiring subset and intersection existence
   5. Theorems requiring empty set existence
3. ZF Set Theory - add the Axiom of Power Sets
   1. Introduce the Axiom of Power Sets
   2. Derive the Axiom of Pairing
   3. Ordered pair theorem
   4. Ordered-pair class abstractions (cont.)
   5. Power class of union and intersection
   6. The identity relation
   7. The membership relation (or epsilon relation)
   8. Partial and total orderings
   9. Founded and well-ordering relations
   10. Relations
   11. The Predecessor Class
   12. Well-founded induction
   13. Ordinals
   14. Definite description binder (inverted iota)
   15. Functions
   16. Cantor's Theorem
   17. Restricted iota (description binder)
   18. Operations
   19. Maps-to notation
   20. Function operation
   21. Proper subset relation
4. ZF Set Theory - add the Axiom of Union
   1. Introduce the Axiom of Union
   2. Ordinals (continued)
   3. Transfinite induction
   4. The natural numbers (i.e., finite ordinals)
   5. Peano's postulates
   6. Finite induction (for finite ordinals)
   7. Relations and functions (cont.)
   8. First and second members of an ordered pair
   9. The support of functions
   10. Special maps-to operations
   11. Function transposition
   12. Curry and uncurry
   13. Undefined values
   14. Well-founded recursion
   15. Functions on ordinals; strictly monotone ordinal functions
   16. "Strong" transfinite recursion
   17. Recursive definition generator
   18. Finite recursion
   19. Ordinal arithmetic
   20. Natural number arithmetic
   21. Equivalence relations and classes
   22. The mapping operation
   23. Infinite Cartesian products
   24. Equinumerosity
   25. Schroeder-Bernstein Theorem
   26. Equinumerosity (cont.)
   27. Pigeonhole Principle
   28. Finite sets
   29. Finitely supported functions
   30. Finite intersections
   31. Hall's marriage theorem
   32. Supremum and infimum
   33. Ordinal isomorphism, Hartogs's theorem
   34. Hartogs function, order types, weak dominance
5. ZF Set Theory - add the Axiom of Regularity
   1. Introduce the Axiom of Regularity
   2. Axiom of Infinity equivalents
6. ZF Set Theory - add the Axiom of Infinity
   1. Introduce the Axiom of Infinity
   2. Existence of omega (the set of natural numbers)
   3. Cantor normal form
   4. Transitive closure
   5. Rank
   6. Scott's trick; collection principle; Hilbert's epsilon
   7. Disjoint union
   8. Cardinal numbers
   9. Axiom of Choice equivalents
   10. Cardinal number arithmetic
   11. The Ackermann bijection
   12. Cofinality (without Axiom of Choice)
   13. Eight inequivalent definitions of finite set
   14. Hereditarily size-limited sets without Choice