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

Theorem limelon 6448
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 6444 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6392 . . 3 (𝐴𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2imbitrrid 246 . 2 (𝐴𝐵 → (Lim 𝐴𝐴 ∈ On))
43imp 406 1 ((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  Ord word 6383  Oncon0 6384  Lim wlim 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389
This theorem is referenced by:  onzsl  7867  limuni3  7873  tfindsg2  7883  dfom2  7889  rdglim  8466  oalim  8570  omlim  8571  oelim  8572  oalimcl  8598  oaass  8599  omlimcl  8616  odi  8617  omass  8618  oen0  8624  oewordri  8630  oelim2  8633  oelimcl  8638  omabs  8689  r1lim  9812  alephordi  10114  cflm  10290  alephsing  10316  pwcfsdom  10623  winafp  10737  r1limwun  10776  omlimcl2  43254  oeord2lim  43322
  Copyright terms: Public domain W3C validator