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 6243 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
2 | elong 6192 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴)) | |
3 | 1, 2 | syl5ibr 247 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On)) |
4 | 3 | imp 407 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 Ord word 6183 Oncon0 6184 Lim wlim 6185 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-in 3940 df-ss 3949 df-uni 4831 df-tr 5164 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-ord 6187 df-on 6188 df-lim 6189 |
This theorem is referenced by: onzsl 7550 limuni3 7556 tfindsg2 7565 dfom2 7571 rdglim 8051 oalim 8146 omlim 8147 oelim 8148 oalimcl 8175 oaass 8176 omlimcl 8193 odi 8194 omass 8195 oen0 8201 oewordri 8207 oelim2 8210 oelimcl 8215 omabs 8263 r1lim 9189 alephordi 9488 cflm 9660 alephsing 9686 pwcfsdom 9993 winafp 10107 r1limwun 10146 |
Copyright terms: Public domain | W3C validator |