|   | 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 6443 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
| 2 | elong 6391 | . . 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 2107 Ord word 6382 Oncon0 6383 Lim wlim 6384 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-v 3481 df-ss 3967 df-uni 4907 df-tr 5259 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-ord 6386 df-on 6387 df-lim 6388 | 
| This theorem is referenced by: onzsl 7868 limuni3 7874 tfindsg2 7884 dfom2 7890 rdglim 8467 oalim 8571 omlim 8572 oelim 8573 oalimcl 8599 oaass 8600 omlimcl 8617 odi 8618 omass 8619 oen0 8625 oewordri 8631 oelim2 8634 oelimcl 8639 omabs 8690 r1lim 9813 alephordi 10115 cflm 10291 alephsing 10317 pwcfsdom 10624 winafp 10738 r1limwun 10777 omlimcl2 43259 oeord2lim 43327 | 
| Copyright terms: Public domain | W3C validator |