![]() |
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 6446 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
2 | elong 6394 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴)) | |
3 | 1, 2 | imbitrrid 246 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On)) |
4 | 3 | imp 406 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2106 Ord word 6385 Oncon0 6386 Lim wlim 6387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-v 3480 df-ss 3980 df-uni 4913 df-tr 5266 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-ord 6389 df-on 6390 df-lim 6391 |
This theorem is referenced by: onzsl 7867 limuni3 7873 tfindsg2 7883 dfom2 7889 rdglim 8465 oalim 8569 omlim 8570 oelim 8571 oalimcl 8597 oaass 8598 omlimcl 8615 odi 8616 omass 8617 oen0 8623 oewordri 8629 oelim2 8632 oelimcl 8637 omabs 8688 r1lim 9810 alephordi 10112 cflm 10288 alephsing 10314 pwcfsdom 10621 winafp 10735 r1limwun 10774 omlimcl2 43231 oeord2lim 43299 |
Copyright terms: Public domain | W3C validator |