![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limelon | Structured version Visualization version Unicode version |
Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
Ref | Expression |
---|---|
limelon |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limord 5501 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elong 5450 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5ibr 229 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | imp 435 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ral 2754 df-rex 2755 df-v 3059 df-in 3423 df-ss 3430 df-uni 4213 df-tr 4512 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-ord 5445 df-on 5446 df-lim 5447 |
This theorem is referenced by: onzsl 6700 limuni3 6706 tfindsg2 6715 dfom2 6721 rdglim 7170 oalim 7260 omlim 7261 oelim 7262 oalimcl 7287 oaass 7288 omlimcl 7305 odi 7306 omass 7307 oen0 7313 oewordri 7319 oelim2 7322 oelimcl 7327 omabs 7374 r1lim 8269 alephordi 8531 cflm 8706 alephsing 8732 pwcfsdom 9034 winafp 9148 r1limwun 9187 |
Copyright terms: Public domain | W3C validator |