Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  limelon Structured version   Visualization version   GIF version

Theorem limelon 6223
 Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
Assertion
Ref Expression
limelon ((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Proof of Theorem limelon
StepHypRef Expression
1 limord 6219 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6168 . . 3 (𝐴𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2syl5ibr 249 . 2 (𝐴𝐵 → (Lim 𝐴𝐴 ∈ On))
43imp 410 1 ((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  Ord word 6159  Oncon0 6160  Lim wlim 6161 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4802  df-tr 5138  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-ord 6163  df-on 6164  df-lim 6165 This theorem is referenced by:  onzsl  7544  limuni3  7550  tfindsg2  7559  dfom2  7565  rdglim  8048  oalim  8143  omlim  8144  oelim  8145  oalimcl  8172  oaass  8173  omlimcl  8190  odi  8191  omass  8192  oen0  8198  oewordri  8204  oelim2  8207  oelimcl  8212  omabs  8260  r1lim  9188  alephordi  9488  cflm  9664  alephsing  9690  pwcfsdom  9997  winafp  10111  r1limwun  10150
 Copyright terms: Public domain W3C validator