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

Theorem limord 4574
Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
Assertion
Ref Expression
limord  |-  ( Lim 
A  ->  Ord  A )

Proof of Theorem limord
StepHypRef Expression
1 df-lim 4520 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp1bi 972 1  |-  ( Lim 
A  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2543   (/)c0 3564   U.cuni 3950   Ord word 4514   Lim wlim 4516
This theorem is referenced by:  0ellim  4577  limelon  4578  nlimsucg  4755  ordzsl  4758  limsuc  4762  limsssuc  4763  limomss  4783  ordom  4787  limom  4793  tfr2b  6586  rdgsucg  6610  rdglimg  6612  rdglim2  6619  oesuclem  6698  odi  6751  omeulem1  6754  oelim2  6767  oeoalem  6768  oeoelem  6770  limenpsi  7211  limensuci  7212  ordtypelem3  7415  ordtypelem5  7417  ordtypelem6  7418  ordtypelem7  7419  ordtypelem9  7421  r1tr  7628  r1ordg  7630  r1ord3g  7631  r1pwss  7636  r1val1  7638  rankwflemb  7645  r1elwf  7648  rankr1ai  7650  rankr1ag  7654  rankr1bg  7655  unwf  7662  rankr1clem  7672  rankr1c  7673  rankval3b  7678  rankonidlem  7680  onssr1  7683  coflim  8067  cflim3  8068  cflim2  8069  cfss  8071  cfslb  8072  cfslbn  8073  cfslb2n  8074  r1limwun  8537  inar1  8576  rdgprc  25168  limitssson  25468  limsucncmpi  25902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-lim 4520
  Copyright terms: Public domain W3C validator