![]() |
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 6375 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
2 | elong 6323 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴)) | |
3 | 1, 2 | syl5ibr 245 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On)) |
4 | 3 | imp 407 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 Ord word 6314 Oncon0 6315 Lim wlim 6316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1089 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-v 3445 df-in 3915 df-ss 3925 df-uni 4864 df-tr 5221 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-ord 6318 df-on 6319 df-lim 6320 |
This theorem is referenced by: onzsl 7774 limuni3 7780 tfindsg2 7790 dfom2 7796 rdglim 8364 oalim 8470 omlim 8471 oelim 8472 oalimcl 8499 oaass 8500 omlimcl 8517 odi 8518 omass 8519 oen0 8525 oewordri 8531 oelim2 8534 oelimcl 8539 omabs 8589 r1lim 9666 alephordi 9968 cflm 10144 alephsing 10170 pwcfsdom 10477 winafp 10591 r1limwun 10630 omlimcl2 41479 oeord2lim 41545 |
Copyright terms: Public domain | W3C validator |