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

Theorem limelon 6379
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 6375 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6323 . . 3 (𝐴𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2syl5ibr 245 . 2 (𝐴𝐵 → (Lim 𝐴𝐴 ∈ On))
43imp 407 1 ((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  Ord word 6314  Oncon0 6315  Lim wlim 6316
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-v 3445  df-in 3915  df-ss 3925  df-uni 4864  df-tr 5221  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6318  df-on 6319  df-lim 6320
This theorem is referenced by:  onzsl  7774  limuni3  7780  tfindsg2  7790  dfom2  7796  rdglim  8364  oalim  8470  omlim  8471  oelim  8472  oalimcl  8499  oaass  8500  omlimcl  8517  odi  8518  omass  8519  oen0  8525  oewordri  8531  oelim2  8534  oelimcl  8539  omabs  8589  r1lim  9666  alephordi  9968  cflm  10144  alephsing  10170  pwcfsdom  10477  winafp  10591  r1limwun  10630  omlimcl2  41479  oeord2lim  41545
  Copyright terms: Public domain W3C validator