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

Theorem limelon 6276
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 6272 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 6221 . . 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 2110  Ord word 6212  Oncon0 6213  Lim wlim 6214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-tr 5162  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-ord 6216  df-on 6217  df-lim 6218
This theorem is referenced by:  onzsl  7625  limuni3  7631  tfindsg2  7640  dfom2  7646  rdglim  8162  oalim  8259  omlim  8260  oelim  8261  oalimcl  8288  oaass  8289  omlimcl  8306  odi  8307  omass  8308  oen0  8314  oewordri  8320  oelim2  8323  oelimcl  8328  omabs  8376  r1lim  9388  alephordi  9688  cflm  9864  alephsing  9890  pwcfsdom  10197  winafp  10311  r1limwun  10350
  Copyright terms: Public domain W3C validator