Metamath Proof Explorer

Table of Contents - 2.4.23. Ordinal arithmetic

  1. c1o
  2. c2o
  3. c3o
  4. c4o
  5. coa
  6. comu
  7. coe
  8. df-1o
  9. df-2o
  10. df-3o
  11. df-4o
  12. df-oadd
  13. df-omul
  14. df-oexp
  15. df1o2
  16. df2o3
  17. df2o2
  18. 1oex
  19. 2oex
  20. 1on
  21. 1onOLD
  22. 2on
  23. 2onOLD
  24. 2on0
  25. ord3
  26. 3on
  27. 4on
  28. 1oexOLD
  29. 2oexOLD
  30. 1n0
  31. nlim1
  32. nlim2
  33. xp01disj
  34. xp01disjl
  35. ordgt0ge1
  36. ordge1n0
  37. el1o
  38. ord1eln01
  39. ord2eln012
  40. 1ellim
  41. 2ellim
  42. dif1o
  43. ondif1
  44. ondif2
  45. 2oconcl
  46. 0lt1o
  47. dif20el
  48. 0we1
  49. brwitnlem
  50. fnoa
  51. fnom
  52. fnoe
  53. oav
  54. omv
  55. oe0lem
  56. oev
  57. oevn0
  58. oa0
  59. om0
  60. oe0m
  61. om0x
  62. oe0m0
  63. oe0m1
  64. oe0
  65. oev2
  66. oasuc
  67. oesuclem
  68. omsuc
  69. oesuc
  70. onasuc
  71. onmsuc
  72. onesuc
  73. oa1suc
  74. oalim
  75. omlim
  76. oelim
  77. oacl
  78. omcl
  79. oecl
  80. oa0r
  81. om0r
  82. o1p1e2
  83. o2p2e4
  84. om1
  85. om1r
  86. oe1
  87. oe1m
  88. oaordi
  89. oaord
  90. oacan
  91. oaword
  92. oawordri
  93. oaord1
  94. oaword1
  95. oaword2
  96. oawordeulem
  97. oawordeu
  98. oawordexr
  99. oawordex
  100. oaordex
  101. oa00
  102. oalimcl
  103. oaass
  104. oarec
  105. oaf1o
  106. oacomf1olem
  107. oacomf1o
  108. omordi
  109. omord2
  110. omord
  111. omcan
  112. omword
  113. omwordi
  114. omwordri
  115. omword1
  116. omword2
  117. om00
  118. om00el
  119. omordlim
  120. omlimcl
  121. odi
  122. omass
  123. oneo
  124. omeulem1
  125. omeulem2
  126. omopth2
  127. omeu
  128. oen0
  129. oeordi
  130. oeord
  131. oecan
  132. oeword
  133. oewordi
  134. oewordri
  135. oeworde
  136. oeordsuc
  137. oelim2
  138. oeoalem
  139. oeoa
  140. oeoelem
  141. oeoe
  142. oelimcl
  143. oeeulem
  144. oeeui
  145. oeeu