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