Metamath Proof Explorer

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