Metamath Proof Explorer


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