Metamath Proof Explorer
Table of Contents - 2.4.20. Ordinal arithmetic
- c1o
- c2o
- c3o
- c4o
- coa
- comu
- coe
- df-1o
- df-2o
- df-3o
- df-4o
- df-oadd
- df-omul
- df-oexp
- df1o2
- df2o3
- df2o2
- 1oex
- 2oex
- 1on
- 1onOLD
- 2on
- 2onOLD
- 2on0
- 3on
- 4on
- 1oexOLD
- 2oexOLD
- 1n0
- xp01disj
- xp01disjl
- ordgt0ge1
- ordge1n0
- el1o
- dif1o
- ondif1
- ondif2
- 2oconcl
- 0lt1o
- dif20el
- 0we1
- brwitnlem
- fnoa
- fnom
- fnoe
- oav
- omv
- oe0lem
- oev
- oevn0
- oa0
- om0
- oe0m
- om0x
- oe0m0
- oe0m1
- oe0
- oev2
- oasuc
- oesuclem
- omsuc
- oesuc
- onasuc
- onmsuc
- onesuc
- oa1suc
- oalim
- omlim
- oelim
- oacl
- omcl
- oecl
- oa0r
- om0r
- o1p1e2
- o2p2e4
- o2p2e4OLD
- om1
- om1r
- oe1
- oe1m
- oaordi
- oaord
- oacan
- oaword
- oawordri
- oaord1
- oaword1
- oaword2
- oawordeulem
- oawordeu
- oawordexr
- oawordex
- oaordex
- oa00
- oalimcl
- oaass
- oarec
- oaf1o
- oacomf1olem
- oacomf1o
- omordi
- omord2
- omord
- omcan
- omword
- omwordi
- omwordri
- omword1
- omword2
- om00
- om00el
- omordlim
- omlimcl
- odi
- omass
- oneo
- omeulem1
- omeulem2
- omopth2
- omeu
- oen0
- oeordi
- oeord
- oecan
- oeword
- oewordi
- oewordri
- oeworde
- oeordsuc
- oelim2
- oeoalem
- oeoa
- oeoelem
- oeoe
- oelimcl
- oeeulem
- oeeui
- oeeu