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

Theorem limord 4942
 Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
Assertion
Ref Expression
limord

Proof of Theorem limord
StepHypRef Expression
1 df-lim 4888 . 2
21simp1bi 1011 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652   c0 3784  U.cuni 4249  Ordword 4882  Limwlim 4884 This theorem is referenced by:  0ellim  4945  limelon  4946  nlimsucg  6677  ordzsl  6680  limsuc  6684  limsssuc  6685  limomss  6705  ordom  6709  limom  6715  tfr2b  7084  rdgsucg  7108  rdglimg  7110  rdglim2  7117  oesuclem  7194  odi  7247  omeulem1  7250  oelim2  7263  oeoalem  7264  oeoelem  7266  limenpsi  7712  limensuci  7713  ordtypelem3  7966  ordtypelem5  7968  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  r1tr  8215  r1ordg  8217  r1ord3g  8218  r1pwss  8223  r1val1  8225  rankwflemb  8232  r1elwf  8235  rankr1ai  8237  rankr1ag  8241  rankr1bg  8242  unwf  8249  rankr1clem  8259  rankr1c  8260  rankval3b  8265  rankonidlem  8267  onssr1  8270  coflim  8662  cflim3  8663  cflim2  8664  cfss  8666  cfslb  8667  cfslbn  8668  cfslb2n  8669  r1limwun  9135  inar1  9174  rdgprc  29227  limsucncmpi  29910 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-lim 4888
 Copyright terms: Public domain W3C validator