Theorem limord 4927

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

Syntax hints:   -> wi 4   = wceq 1383   =/= wne 2638   (/)c0 3770   U.cuni 4234   Ord word 4867   Lim wlim 4869

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 976  df-lim 4873

This theorem is referenced by:  0ellim  4930  limelon  4931  nlimsucg  6662  ordzsl  6665  limsuc  6669  limsssuc  6670  limomss  6690  ordom  6694  limom  6700  tfr2b  7067  rdgsucg  7091  rdglimg  7093  rdglim2  7100  oesuclem  7177  odi  7230  omeulem1  7233  oelim2  7246  oeoalem  7247  oeoelem  7249  limenpsi  7694  limensuci  7695  ordtypelem3  7948  ordtypelem5  7950  ordtypelem6  7951  ordtypelem7  7952  ordtypelem9  7954  r1tr  8197  r1ordg  8199  r1ord3g  8200  r1pwss  8205  r1val1  8207  rankwflemb  8214  r1elwf  8217  rankr1ai  8219  rankr1ag  8223  rankr1bg  8224  unwf  8231  rankr1clem  8241  rankr1c  8242  rankval3b  8247  rankonidlem  8249  onssr1  8252  coflim  8644  cflim3  8645  cflim2  8646  cfss  8648  cfslb  8649  cfslbn  8650  cfslb2n  8651  r1limwun  9117  inar1  9156  rdgprc  29203  limsucncmpi  29886