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