Metamath Proof Explorer


Table of Contents - 20.44. Mathbox for Zhi Wang

  1. Propositional calculus
    1. pm4.71da
    2. logic1
    3. logic1a
    4. logic2
    5. pm5.32dav
    6. pm5.32dra
    7. exp12bd
    8. mpbiran3d
    9. mpbiran4d
  2. Predicate calculus with equality
    1. Axiom scheme ax-5 (Distinctness)
  3. ZF Set Theory - start with the Axiom of Extensionality
    1. Restricted quantification
    2. The empty set
    3. Unordered and ordered pairs
    4. The union of a class
  4. ZF Set Theory - add the Axiom of Replacement
    1. Theorems requiring subset and intersection existence
  5. ZF Set Theory - add the Axiom of Power Sets
    1. Functions
    2. Operations
  6. ZF Set Theory - add the Axiom of Union
    1. Equinumerosity
  7. Order sets
    1. Real number intervals
  8. Moore spaces
    1. mreuniss
  9. Topology
    1. Closure and interior
    2. Neighborhoods
    3. Subspace topologies
    4. Limits and continuity in topological spaces
    5. Topological definitions using the reals
    6. Separated sets
    7. Separated spaces: T0, T1, T2 (Hausdorff) ...
  10. Preordered sets and directed sets using extensible structures
    1. isprsd
  11. Posets and lattices using extensible structures
    1. Posets
    2. Lattices
    3. Subset order structures
  12. Categories
    1. Categories
    2. Monomorphisms and epimorphisms
    3. Functors
  13. Examples of categories
    1. Thin categories
    2. Preordered sets as thin categories
    3. Monoids as categories