Theorem limord 5485

Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limord	|- ( Lim A -> Ord A )

Proof of Theorem limord

Step	Hyp	Ref	Expression
1		df-lim 5431	. 2 |- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
2	1	simp1bi 1024	1 |- ( Lim A -> Ord A )

Syntax hints:   -> wi 4   = wceq 1446   =/= wne 2624   (/)c0 3733   U.cuni 4201   Ord word 5425   Lim 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