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

Theorem limord 4467
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 4413 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp1bi 970 1  |-  ( Lim 
A  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459   (/)c0 3468   U.cuni 3843   Ord word 4407   Lim wlim 4409
This theorem is referenced by:  0ellim  4470  limelon  4471  nlimsucg  4649  ordzsl  4652  limsuc  4656  limsssuc  4657  limomss  4677  ordom  4681  limom  4687  tfr2b  6428  rdgsucg  6452  rdglimg  6454  rdglim2  6461  oesuclem  6540  odi  6593  omeulem1  6596  oelim2  6609  oeoalem  6610  oeoelem  6612  limenpsi  7052  limensuci  7053  ordtypelem3  7251  ordtypelem5  7253  ordtypelem6  7254  ordtypelem7  7255  ordtypelem9  7257  r1tr  7464  r1ordg  7466  r1ord3g  7467  r1pwss  7472  r1val1  7474  rankwflemb  7481  r1elwf  7484  rankr1ai  7486  rankr1ag  7490  rankr1bg  7491  unwf  7498  rankr1clem  7508  rankr1c  7509  rankval3b  7514  rankonidlem  7516  onssr1  7519  coflim  7903  cflim3  7904  cflim2  7905  cfss  7907  cfslb  7908  cfslbn  7909  cfslb2n  7910  r1limwun  8374  inar1  8413  rdgprc  24222  limitssson  24522  limsucncmpi  24956
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 177  df-an 360  df-3an 936  df-lim 4413
  Copyright terms: Public domain W3C validator