Metamath Proof Explorer


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