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

Theorem limord 5485
 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 5431 . 2
21simp1bi 1024 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1446   wne 2624  c0 3733  cuni 4201   word 5425   wlim 5427 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 189  df-an 373  df-3an 988  df-lim 5431 This theorem is referenced by:  0ellim  5488  limelon  5489  nlimsucg  6674  ordzsl  6677  limsuc  6681  limsssuc  6682  limomss  6702  ordom  6706  limom  6712  tfr2b  7119  rdgsucg  7146  rdglimg  7148  rdglim2  7155  oesuclem  7232  odi  7285  omeulem1  7288  oelim2  7301  oeoalem  7302  oeoelem  7304  limenpsi  7752  limensuci  7753  ordtypelem3  8040  ordtypelem5  8042  ordtypelem6  8043  ordtypelem7  8044  ordtypelem9  8046  r1tr  8252  r1ordg  8254  r1ord3g  8255  r1pwss  8260  r1val1  8262  rankwflemb  8269  r1elwf  8272  rankr1ai  8274  rankr1ag  8278  rankr1bg  8279  unwf  8286  rankr1clem  8296  rankr1c  8297  rankval3b  8302  rankonidlem  8304  onssr1  8307  coflim  8696  cflim3  8697  cflim2  8698  cfss  8700  cfslb  8701  cfslbn  8702  cfslb2n  8703  r1limwun  9166  inar1  9205  rdgprc  30453  limsucncmpi  31117
 Copyright terms: Public domain W3C validator