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

Theorem limelon 6447
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 6443 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6391 . . 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 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