Metamath Proof Explorer
Table of Contents - 2.4.2. Ordinals (continued)
- epweon
- ordon
- onprc
- ssorduni
- ssonuni
- ssonunii
- ordeleqon
- ordsson
- onss
- predon
- predonOLD
- ssonprc
- onuni
- orduni
- onint
- onint0
- onssmin
- onminesb
- onminsb
- oninton
- onintrab
- onintrab2
- onnmin
- onnminsb
- oneqmin
- uniordint
- onminex
- sucon
- sucexb
- sucexg
- sucex
- onmindif2
- suceloni
- ordsuc
- ordpwsuc
- onpwsuc
- sucelon
- ordsucss
- onpsssuc
- ordelsuc
- onsucmin
- ordsucelsuc
- ordsucsssuc
- ordsucuniel
- ordsucun
- ordunpr
- ordunel
- onsucuni
- ordsucuni
- orduniorsuc
- unon
- ordunisuc
- orduniss2
- onsucuni2
- 0elsuc
- limon
- onssi
- onsuci
- onuniorsuci
- onuninsuci
- onsucssi
- nlimsucg
- orduninsuc
- ordunisuc2
- ordzsl
- onzsl
- dflim3
- dflim4
- limsuc
- limsssuc
- nlimon
- limuni3