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