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

Theorem limelon 5931
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 5927 . . 3 (Lim 𝐴 → Ord 𝐴)
2 elong 5874 . . 3 (𝐴𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2syl5ibr 236 . 2 (𝐴𝐵 → (Lim 𝐴𝐴 ∈ On))
43imp 393 1 ((𝐴𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2144  Ord word 5865  Oncon0 5866  Lim wlim 5867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-in 3728  df-ss 3735  df-uni 4573  df-tr 4885  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-lim 5871
This theorem is referenced by:  onzsl  7192  limuni3  7198  tfindsg2  7207  dfom2  7213  rdglim  7674  oalim  7765  omlim  7766  oelim  7767  oalimcl  7793  oaass  7794  omlimcl  7811  odi  7812  omass  7813  oen0  7819  oewordri  7825  oelim2  7828  oelimcl  7833  omabs  7880  r1lim  8798  alephordi  9096  cflm  9273  alephsing  9299  pwcfsdom  9606  winafp  9720  r1limwun  9759
  Copyright terms: Public domain W3C validator