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. Induction on Cartesian products
   10. Ordering on Cartesian products
   11. Ordering Ordinal Sequences
   12. The support of functions
   13. Special maps-to operations
   14. Function transposition
   15. Curry and uncurry
   16. Undefined values
   17. Well-founded recursion
   18. Well-ordered recursion
   19. Functions on ordinals; strictly monotone ordinal functions
   20. "Strong" transfinite recursion
   21. Recursive definition generator
   22. Finite recursion
   23. Ordinal arithmetic
   24. Natural number arithmetic
   25. Natural addition
   26. Equivalence relations and classes
   27. The mapping operation
   28. Infinite Cartesian products
   29. Equinumerosity
   30. Schroeder-Bernstein Theorem
   31. Equinumerosity (cont.)
   32. Finite sets
   33. Pigeonhole Principle
   34. Finite sets (cont.)
   35. Finitely supported functions
   36. Finite intersections
   37. Hall's marriage theorem
   38. Supremum and infimum
   39. Ordinal isomorphism, Hartogs's theorem
   40. Hartogs function
   41. 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
   6. Well-Founded Induction
   7. Well-Founded Recursion
   8. Rank
   9. Scott's trick; collection principle; Hilbert's epsilon
   10. Disjoint union
   11. Cardinal numbers
   12. Axiom of Choice equivalents
   13. Cardinal number arithmetic
   14. The Ackermann bijection
   15. Cofinality (without Axiom of Choice)
   16. Eight inequivalent definitions of finite set
   17. Hereditarily size-limited sets without Choice