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

Theorem limord 4632
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 4578 . 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 1652    =/= wne 2598   (/)c0 3620   U.cuni 4007   Ord word 4572   Lim wlim 4574
This theorem is referenced by:  0ellim  4635  limelon  4636  nlimsucg  4814  ordzsl  4817  limsuc  4821  limsssuc  4822  limomss  4842  ordom  4846  limom  4852  tfr2b  6649  rdgsucg  6673  rdglimg  6675  rdglim2  6682  oesuclem  6761  odi  6814  omeulem1  6817  oelim2  6830  oeoalem  6831  oeoelem  6833  limenpsi  7274  limensuci  7275  ordtypelem3  7481  ordtypelem5  7483  ordtypelem6  7484  ordtypelem7  7485  ordtypelem9  7487  r1tr  7694  r1ordg  7696  r1ord3g  7697  r1pwss  7702  r1val1  7704  rankwflemb  7711  r1elwf  7714  rankr1ai  7716  rankr1ag  7720  rankr1bg  7721  unwf  7728  rankr1clem  7738  rankr1c  7739  rankval3b  7744  rankonidlem  7746  onssr1  7749  coflim  8133  cflim3  8134  cflim2  8135  cfss  8137  cfslb  8138  cfslbn  8139  cfslb2n  8140  r1limwun  8603  inar1  8642  rdgprc  25414  limsucncmpi  26187
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 4578
  Copyright terms: Public domain W3C validator