Theorem limord 4937

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

Syntax hints:   -> wi 4   = wceq 1379   =/= wne 2662   (/)c0 3785   U.cuni 4245   Ord word 4877   Lim wlim 4879

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 975  df-lim 4883

This theorem is referenced by:  0ellim  4940  limelon  4941  nlimsucg  6655  ordzsl  6658  limsuc  6662  limsssuc  6663  limomss  6683  ordom  6687  limom  6693  tfr2b  7062  rdgsucg  7086  rdglimg  7088  rdglim2  7095  oesuclem  7172  odi  7225  omeulem1  7228  oelim2  7241  oeoalem  7242  oeoelem  7244  limenpsi  7689  limensuci  7690  ordtypelem3  7941  ordtypelem5  7943  ordtypelem6  7944  ordtypelem7  7945  ordtypelem9  7947  r1tr  8190  r1ordg  8192  r1ord3g  8193  r1pwss  8198  r1val1  8200  rankwflemb  8207  r1elwf  8210  rankr1ai  8212  rankr1ag  8216  rankr1bg  8217  unwf  8224  rankr1clem  8234  rankr1c  8235  rankval3b  8240  rankonidlem  8242  onssr1  8245  coflim  8637  cflim3  8638  cflim2  8639  cfss  8641  cfslb  8642  cfslbn  8643  cfslb2n  8644  r1limwun  9110  inar1  9149  rdgprc  28801  limsucncmpi  29484