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

Theorem limelon 6247
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 6243 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6192 . . 3 (𝐴𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2syl5ibr 247 . 2 (𝐴𝐵 → (Lim 𝐴𝐴 ∈ On))
43imp 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