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

Theorem limord 4451
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 4397 . 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 1623    =/= wne 2446   (/)c0 3455   U.cuni 3827   Ord word 4391   Lim wlim 4393
This theorem is referenced by:  0ellim  4454  limelon  4455  nlimsucg  4633  ordzsl  4636  limsuc  4640  limsssuc  4641  limomss  4661  ordom  4665  limom  4671  tfr2b  6412  rdgsucg  6436  rdglimg  6438  rdglim2  6445  oesuclem  6524  odi  6577  omeulem1  6580  oelim2  6593  oeoalem  6594  oeoelem  6596  limenpsi  7036  limensuci  7037  ordtypelem3  7235  ordtypelem5  7237  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  r1tr  7448  r1ordg  7450  r1ord3g  7451  r1pwss  7456  r1val1  7458  rankwflemb  7465  r1elwf  7468  rankr1ai  7470  rankr1ag  7474  rankr1bg  7475  unwf  7482  rankr1clem  7492  rankr1c  7493  rankval3b  7498  rankonidlem  7500  onssr1  7503  coflim  7887  cflim3  7888  cflim2  7889  cfss  7891  cfslb  7892  cfslbn  7893  cfslb2n  7894  r1limwun  8358  inar1  8397  rdgprc  24151  limitssson  24451  limsucncmpi  24884
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 4397
  Copyright terms: Public domain W3C validator