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

Theorem limelon 4612
Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
Assertion
Ref Expression
limelon  |-  ( ( A  e.  B  /\  Lim  A )  ->  A  e.  On )

Proof of Theorem limelon
StepHypRef Expression
1 limord 4608 . . 3  |-  ( Lim 
A  ->  Ord  A )
2 elong 4557 . . 3  |-  ( A  e.  B  ->  ( A  e.  On  <->  Ord  A ) )
31, 2syl5ibr 213 . 2  |-  ( A  e.  B  ->  ( Lim  A  ->  A  e.  On ) )
43imp 419 1  |-  ( ( A  e.  B  /\  Lim  A )  ->  A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   Ord word 4548   Oncon0 4549   Lim wlim 4550
This theorem is referenced by:  onzsl  4793  limuni3  4799  tfindsg2  4808  dfom2  4814  rdglim  6651  oalim  6743  omlim  6744  oelim  6745  oalimcl  6770  oaass  6771  omlimcl  6788  odi  6789  omass  6790  oen0  6796  oewordri  6802  oelim2  6805  oelimcl  6810  omabs  6857  r1lim  7662  alephordi  7919  cflm  8094  alephsing  8120  pwcfsdom  8422  winafp  8536  r1limwun  8575
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680  df-v 2926  df-in 3295  df-ss 3302  df-uni 3984  df-tr 4271  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554
  Copyright terms: Public domain W3C validator