![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limelon | Structured version Visualization version GIF version |
Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.) |
Ref | Expression |
---|---|
limelon | ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limord 6088 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
2 | elong 6037 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴)) | |
3 | 1, 2 | syl5ibr 238 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On)) |
4 | 3 | imp 398 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 Ord word 6028 Oncon0 6029 Lim wlim 6030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-in 3836 df-ss 3843 df-uni 4713 df-tr 5031 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-ord 6032 df-on 6033 df-lim 6034 |
This theorem is referenced by: onzsl 7377 limuni3 7383 tfindsg2 7392 dfom2 7398 rdglim 7866 oalim 7959 omlim 7960 oelim 7961 oalimcl 7987 oaass 7988 omlimcl 8005 odi 8006 omass 8007 oen0 8013 oewordri 8019 oelim2 8022 oelimcl 8027 omabs 8074 r1lim 8995 alephordi 9294 cflm 9470 alephsing 9496 pwcfsdom 9803 winafp 9917 r1limwun 9956 |
Copyright terms: Public domain | W3C validator |