![]() |
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 5927 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
2 | elong 5874 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴)) | |
3 | 1, 2 | syl5ibr 236 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On)) |
4 | 3 | imp 393 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∈ wcel 2144 Ord word 5865 Oncon0 5866 Lim wlim 5867 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-v 3351 df-in 3728 df-ss 3735 df-uni 4573 df-tr 4885 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-ord 5869 df-on 5870 df-lim 5871 |
This theorem is referenced by: onzsl 7192 limuni3 7198 tfindsg2 7207 dfom2 7213 rdglim 7674 oalim 7765 omlim 7766 oelim 7767 oalimcl 7793 oaass 7794 omlimcl 7811 odi 7812 omass 7813 oen0 7819 oewordri 7825 oelim2 7828 oelimcl 7833 omabs 7880 r1lim 8798 alephordi 9096 cflm 9273 alephsing 9299 pwcfsdom 9606 winafp 9720 r1limwun 9759 |
Copyright terms: Public domain | W3C validator |