![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ordelon | Structured version Unicode version |
Description: An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
Ref | Expression |
---|---|
ordelon |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordelord 4836 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elong 4822 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantl 466 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbird 232 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4508 ax-nul 4516 ax-pr 4626 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2599 df-ne 2644 df-ral 2798 df-rex 2799 df-rab 2802 df-v 3067 df-dif 3426 df-un 3428 df-in 3430 df-ss 3437 df-nul 3733 df-if 3887 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4187 df-br 4388 df-opab 4446 df-tr 4481 df-eprel 4727 df-po 4736 df-so 4737 df-fr 4774 df-we 4776 df-ord 4817 df-on 4818 |
This theorem is referenced by: onelon 4839 ordunidif 4862 ordpwsuc 6523 ordsucun 6533 ordunel 6535 ordunisuc2 6552 oesuclem 7062 odi 7115 oelim2 7131 oeoalem 7132 oeoelem 7134 limenpsi 7583 ordtypelem9 7838 oismo 7852 cantnflt 7978 cantnfp1lem3 7986 cantnflem1b 7992 cantnflem1 7995 cantnfltOLD 8008 cantnfp1lem3OLD 8012 cantnflem1bOLD 8015 cantnflem1OLD 8018 rankr1bg 8108 rankr1clem 8125 rankr1c 8126 rankonidlem 8133 infxpenlem 8278 coflim 8528 fin23lem26 8592 fpwwe2lem8 8902 nofulllem5 27978 onsuct0 28418 |
Copyright terms: Public domain | W3C validator |