Theorem limord 4773

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

Syntax hints:   -> wi 4   = wceq 1369   =/= wne 2601   (/)c0 3632   U.cuni 4086   Ord word 4713   Lim wlim 4715

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 967  df-lim 4719

This theorem is referenced by:  0ellim  4776  limelon  4777  nlimsucg  6448  ordzsl  6451  limsuc  6455  limsssuc  6456  limomss  6476  ordom  6480  limom  6486  tfr2b  6847  rdgsucg  6871  rdglimg  6873  rdglim2  6880  oesuclem  6957  odi  7010  omeulem1  7013  oelim2  7026  oeoalem  7027  oeoelem  7029  limenpsi  7478  limensuci  7479  ordtypelem3  7726  ordtypelem5  7728  ordtypelem6  7729  ordtypelem7  7730  ordtypelem9  7732  r1tr  7975  r1ordg  7977  r1ord3g  7978  r1pwss  7983  r1val1  7985  rankwflemb  7992  r1elwf  7995  rankr1ai  7997  rankr1ag  8001  rankr1bg  8002  unwf  8009  rankr1clem  8019  rankr1c  8020  rankval3b  8025  rankonidlem  8027  onssr1  8030  coflim  8422  cflim3  8423  cflim2  8424  cfss  8426  cfslb  8427  cfslbn  8428  cfslb2n  8429  r1limwun  8895  inar1  8934  rdgprc  27559  limsucncmpi  28243