Theorem limord 4885

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

Syntax hints:   -> wi 4   = wceq 1370   =/= wne 2647   (/)c0 3744   U.cuni 4198   Ord word 4825   Lim wlim 4827

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 4831

This theorem is referenced by:  0ellim  4888  limelon  4889  nlimsucg  6562  ordzsl  6565  limsuc  6569  limsssuc  6570  limomss  6590  ordom  6594  limom  6600  tfr2b  6964  rdgsucg  6988  rdglimg  6990  rdglim2  6997  oesuclem  7074  odi  7127  omeulem1  7130  oelim2  7143  oeoalem  7144  oeoelem  7146  limenpsi  7595  limensuci  7596  ordtypelem3  7844  ordtypelem5  7846  ordtypelem6  7847  ordtypelem7  7848  ordtypelem9  7850  r1tr  8093  r1ordg  8095  r1ord3g  8096  r1pwss  8101  r1val1  8103  rankwflemb  8110  r1elwf  8113  rankr1ai  8115  rankr1ag  8119  rankr1bg  8120  unwf  8127  rankr1clem  8137  rankr1c  8138  rankval3b  8143  rankonidlem  8145  onssr1  8148  coflim  8540  cflim3  8541  cflim2  8542  cfss  8544  cfslb  8545  cfslbn  8546  cfslb2n  8547  r1limwun  9013  inar1  9052  rdgprc  27751  limsucncmpi  28434