Theorem limord 5499

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 5445	. 2 |- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
2	1	simp1bi 1021	1 |- ( Lim A -> Ord A )

Syntax hints:   -> wi 4   = wceq 1438   =/= wne 2619   (/)c0 3762   U.cuni 4217   Ord word 5439   Lim wlim 5441

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 985  df-lim 5445

This theorem is referenced by:  0ellim  5502  limelon  5503  nlimsucg  6681  ordzsl  6684  limsuc  6688  limsssuc  6689  limomss  6709  ordom  6713  limom  6719  tfr2b  7120  rdgsucg  7147  rdglimg  7149  rdglim2  7156  oesuclem  7233  odi  7286  omeulem1  7289  oelim2  7302  oeoalem  7303  oeoelem  7305  limenpsi  7751  limensuci  7752  ordtypelem3  8039  ordtypelem5  8041  ordtypelem6  8042  ordtypelem7  8043  ordtypelem9  8045  r1tr  8250  r1ordg  8252  r1ord3g  8253  r1pwss  8258  r1val1  8260  rankwflemb  8267  r1elwf  8270  rankr1ai  8272  rankr1ag  8276  rankr1bg  8277  unwf  8284  rankr1clem  8294  rankr1c  8295  rankval3b  8300  rankonidlem  8302  onssr1  8305  coflim  8693  cflim3  8694  cflim2  8695  cfss  8697  cfslb  8698  cfslbn  8699  cfslb2n  8700  r1limwun  9163  inar1  9202  rdgprc  30442  limsucncmpi  31104