Metamath Proof Explorer

Table of Contents - 20.33. Mathbox for Richard Penner

  1. Short Studies
    1. Additional work on conditional logical operator
    2. Sophisms
    3. Finite Sets
    4. General Observations
    5. Infinite Sets
    6. Finite intersection property
    7. RP ADDTO: Subclasses and subsets
    8. RP ADDTO: The intersection of a class
    9. RP ADDTO: Theorems requiring subset and intersection existence
    10. RP ADDTO: Relations
    11. RP ADDTO: Functions
    12. RP ADDTO: Finite induction (for finite ordinals)
    13. RP ADDTO: First and second members of an ordered pair
    14. RP ADDTO: The reflexive and transitive properties of relations
    15. RP ADDTO: Basic properties of closures
    16. RP REPLACE: Definitions and basic properties of transitive closures
  2. Additional statements on relations and subclasses
    1. al3im
    2. intima0
    3. elimaint
    4. csbcog
    5. cnviun
    6. imaiun1
    7. coiun1
    8. elintima
    9. intimass
    10. intimass2
    11. intimag
    12. intimasn
    13. intimasn2
    14. ss2iundf
    15. ss2iundv
    16. cbviuneq12df
    17. cbviuneq12dv
    18. conrel1d
    19. conrel2d
    20. Transitive relations (not to be confused with transitive classes).
    21. Reflexive closures
    22. Finite relationship composition.
    23. Transitive closure of a relation
    24. Adapted from Frege
  3. Propositions from _Begriffsschrift_
    1. _Begriffsschrift_ Chapter I
    2. _Begriffsschrift_ Notation hints
    3. _Begriffsschrift_ Chapter II Implication
    4. _Begriffsschrift_ Chapter II Implication and Negation
    5. _Begriffsschrift_ Chapter II with logical equivalence
    6. _Begriffsschrift_ Chapter II with equivalence of sets
    7. _Begriffsschrift_ Chapter II with equivalence of classes
    8. _Begriffsschrift_ Chapter III Properties hereditary in a sequence
    9. _Begriffsschrift_ Chapter III Following in a sequence
    10. _Begriffsschrift_ Chapter III Member of sequence
    11. _Begriffsschrift_ Chapter III Single-valued procedures
  4. Exploring Topology via Seifert and Threlfall
    1. Equinumerosity of sets of relations and maps
    2. Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
    3. Generic Neighborhood Spaces
  5. Exploring Higher Homotopy via Kerodon
    1. Simplicial Sets