Metamath Proof Explorer

Table of Contents - 21.38. Mathbox for Richard Penner

1. Set Theory and Ordinal Numbers
   1. uniel
   2. unielss
   3. unielid
   4. ssunib
   5. rp-intrabeq
   6. rp-unirabeq
   7. onmaxnelsup
   8. onsupneqmaxlim0
   9. onsupcl2
   10. onuniintrab
   11. onintunirab
   12. onsupnmax
   13. onsupuni
   14. onsupuni2
   15. onsupintrab
   16. onsupintrab2
   17. onsupcl3
   18. onsupex3
   19. onuniintrab2
   20. oninfint
   21. oninfunirab
   22. oninfcl2
   23. onsupmaxb
   24. onexgt
   25. onexomgt
   26. omlimcl2
   27. onexlimgt
   28. onexoegt
   29. oninfex2
   30. onsupeqmax
   31. onsupeqnmax
   32. onsuplub
   33. onsupnub
   34. onfisupcl
   35. onelord
   36. onepsuc
   37. epsoon
   38. epirron
   39. oneptr
   40. oneltr
   41. oneptri
   42. ordeldif
   43. ordeldifsucon
   44. ordeldif1o
   45. ordne0gt0
   46. ondif1i
   47. onsucelab
   48. dflim6
   49. limnsuc
   50. onsucss
   51. ordnexbtwnsuc
   52. orddif0suc
   53. onsucf1lem
   54. onsucf1olem
   55. onsucrn
   56. onsucf1o
   57. dflim7
   58. onov0suclim
   59. oa0suclim
   60. om0suclim
   61. oe0suclim
   62. oaomoecl
   63. onsupsucismax
   64. onsssupeqcond
   65. limexissup
   66. limiun
   67. limexissupab
   68. om1om1r
   69. oe0rif
   70. oasubex
   71. nnamecl
   72. onsucwordi
   73. oalim2cl
   74. oaltublim
   75. oaordi3
   76. oaord3
   77. 1oaomeqom
   78. oaabsb
   79. oaordnrex
   80. oaordnr
   81. omge1
   82. omge2
   83. omlim2
   84. omord2lim
   85. omord2i
   86. omord2com
   87. 2omomeqom
   88. omnord1ex
   89. omnord1
   90. oege1
   91. oege2
   92. rp-oelim2
   93. oeord2lim
   94. oeord2i
   95. oeord2com
   96. nnoeomeqom
   97. df3o2
   98. df3o3
   99. oenord1ex
   100. oenord1
   101. oaomoencom
   102. oenassex
   103. oenass
   104. cantnftermord
   105. cantnfub
   106. cantnfub2
   107. bropabg
   108. cantnfresb
   109. cantnf2
2. Natural addition of Cantor normal forms
   1. oawordex2
   2. nnawordexg
   3. succlg
   4. dflim5
   5. oacl2g
   6. onmcl
   7. omabs2
   8. omcl2
   9. omcl3g
   10. ordsssucb
   11. tfsconcatlem
   12. tfsconcatun
   13. tfsconcatfn
   14. tfsconcatfv1
   15. tfsconcatfv2
   16. tfsconcatfv
   17. tfsconcatrn
   18. tfsconcatfo
   19. tfsconcatb0
   20. tfsconcat0i
   21. tfsconcat0b
   22. tfsconcat00
   23. tfsconcatrev
   24. tfsconcatrnss12
   25. tfsconcatrnss
   26. tfsconcatrnsson
   27. tfsnfin
   28. rp-tfslim
   29. ofoafg
   30. ofoaf
   31. ofoafo
   32. ofoacl
   33. ofoaid1
   34. ofoaid2
   35. ofoaass
   36. ofoacom
   37. naddcnff
   38. naddcnffn
   39. naddcnffo
   40. naddcnfcl
   41. naddcnfcom
   42. naddcnfid1
   43. naddcnfid2
   44. naddcnfass
   45. onsucunifi
   46. sucunisn
   47. onsucunipr
   48. onsucunitp
   49. oaun3lem1
   50. oaun3lem2
   51. oaun3lem3
   52. oaun3lem4
   53. rp-abid
   54. oadif1lem
   55. oadif1
   56. oaun2
   57. oaun3
   58. naddov4
   59. nadd2rabtr
   60. nadd2rabord
   61. nadd2rabex
   62. nadd2rabon
   63. nadd1rabtr
   64. nadd1rabord
   65. nadd1rabex
   66. nadd1rabon
   67. nadd1suc
   68. naddass1
   69. naddgeoa
   70. naddonnn
   71. naddwordnexlem0
   72. naddwordnexlem1
   73. naddwordnexlem2
   74. naddwordnexlem3
   75. oawordex3
   76. naddwordnexlem4
   77. ordsssucim
   78. insucid
   79. om2
   80. oaltom
   81. oe2
   82. omltoe
3. Surreal Contributions
   1. abeqabi
   2. abpr
   3. abtp
   4. ralopabb
   5. fpwfvss
   6. sdomne0
   7. sdomne0d
   8. safesnsupfiss
   9. safesnsupfiub
   10. safesnsupfidom1o
   11. safesnsupfilb
   12. isoeq145d
   13. resisoeq45d
   14. negslem1
   15. nvocnvb
   16. rp-brsslt
   17. nla0002
   18. nla0003
   19. nla0001
   20. faosnf0.11b
   21. dfno2
   22. onnog
   23. onnobdayg
   24. bdaybndex
   25. bdaybndbday
   26. onno
   27. onnoi
   28. 0no
   29. 1no
   30. 2no
   31. 3no
   32. 4no
   33. fnimafnex
4. Short Studies
   1. nlimsuc
   2. nlim1NEW
   3. nlim2NEW
   4. nlim3
   5. nlim4
   6. oa1un
   7. oa1cl
   8. 0finon
   9. 1finon
   10. 2finon
   11. 3finon
   12. 4finon
   13. finona1cl
   14. finonex
   15. fzunt
   16. fzuntd
   17. fzunt1d
   18. fzuntgd
   19. Additional work on conditional logical operator
   20. Sophisms
   21. Finite Sets
   22. General Observations
   23. Infinite Sets
   24. Finite intersection property
   25. RP ADDTO: Subclasses and subsets
   26. RP ADDTO: The intersection of a class
   27. RP ADDTO: Theorems requiring subset and intersection existence
   28. RP ADDTO: Relations
   29. RP ADDTO: Functions
   30. RP ADDTO: Finite induction (for finite ordinals)
   31. RP ADDTO: First and second members of an ordered pair
   32. RP ADDTO: The reflexive and transitive properties of relations
   33. RP ADDTO: Basic properties of closures
   34. RP REPLACE: Definitions and basic properties of transitive closures
   35. Additions for square root; absolute value
5. Additional statements on relations and subclasses
   1. al3im
   2. intima0
   3. elimaint
   4. cnviun
   5. imaiun1
   6. coiun1
   7. elintima
   8. intimass
   9. intimass2
   10. intimag
   11. intimasn
   12. intimasn2
   13. ss2iundf
   14. ss2iundv
   15. cbviuneq12df
   16. cbviuneq12dv
   17. conrel1d
   18. conrel2d
   19. Transitive relations (not to be confused with transitive classes).
   20. Reflexive closures
   21. Finite relationship composition.
   22. Transitive closure of a relation
   23. Adapted from Frege
6. 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
7. 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
8. Exploring Higher Homotopy via Kerodon
   1. Simplicial Sets