Theorem limord 4851

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

Syntax hints:   -> wi 4   = wceq 1399   =/= wne 2577   (/)c0 3711   U.cuni 4163   Ord word 4791   Lim wlim 4793

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 369  df-3an 973  df-lim 4797

This theorem is referenced by:  0ellim  4854  limelon  4855  nlimsucg  6576  ordzsl  6579  limsuc  6583  limsssuc  6584  limomss  6604  ordom  6608  limom  6614  tfr2b  6983  rdgsucg  7007  rdglimg  7009  rdglim2  7016  oesuclem  7093  odi  7146  omeulem1  7149  oelim2  7162  oeoalem  7163  oeoelem  7165  limenpsi  7611  limensuci  7612  ordtypelem3  7860  ordtypelem5  7862  ordtypelem6  7863  ordtypelem7  7864  ordtypelem9  7866  r1tr  8107  r1ordg  8109  r1ord3g  8110  r1pwss  8115  r1val1  8117  rankwflemb  8124  r1elwf  8127  rankr1ai  8129  rankr1ag  8133  rankr1bg  8134  unwf  8141  rankr1clem  8151  rankr1c  8152  rankval3b  8157  rankonidlem  8159  onssr1  8162  coflim  8554  cflim3  8555  cflim2  8556  cfss  8558  cfslb  8559  cfslbn  8560  cfslb2n  8561  r1limwun  9025  inar1  9064  rdgprc  29392  limsucncmpi  30063