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 (variant)
   13. Well-ordered induction
   14. Ordinals
   15. Definite description binder (inverted iota)
   16. Functions
   17. Cantor's Theorem
   18. Restricted iota (description binder)
   19. Operations
   20. Maps-to notation
   21. Function operation
   22. 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. Well-ordered recursion
   16. Functions on ordinals; strictly monotone ordinal functions
   17. "Strong" transfinite recursion
   18. Recursive definition generator
   19. Finite recursion
   20. Ordinal arithmetic
   21. Natural number arithmetic
   22. Equivalence relations and classes
   23. The mapping operation
   24. Infinite Cartesian products
   25. Equinumerosity
   26. Schroeder-Bernstein Theorem
   27. Equinumerosity (cont.)
   28. Finite sets
   29. Pigeonhole Principle
   30. Finite sets (cont.)
   31. Finitely supported functions
   32. Finite intersections
   33. Hall's marriage theorem
   34. Supremum and infimum
   35. Ordinal isomorphism, Hartogs's theorem
   36. Hartogs function
   37. 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 of a relation
   5. Transitive closure under a relationship
   6. Transitive closure
   7. Well-Founded Induction
   8. Well-Founded Recursion
   9. Rank
   10. Scott's trick; collection principle; Hilbert's epsilon
   11. Disjoint union
   12. Cardinal numbers
   13. Axiom of Choice equivalents
   14. Cardinal number arithmetic
   15. The Ackermann bijection
   16. Cofinality (without Axiom of Choice)
   17. Eight inequivalent definitions of finite set
   18. Hereditarily size-limited sets without Choice