Theorem limord 4600

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

Syntax hints:   -> wi 4   = wceq 1649   =/= wne 2567   (/)c0 3588   U.cuni 3975   Ord word 4540   Lim wlim 4542

This theorem is referenced by:  0ellim  4603  limelon  4604  nlimsucg  4781  ordzsl  4784  limsuc  4788  limsssuc  4789  limomss  4809  ordom  4813  limom  4819  tfr2b  6616  rdgsucg  6640  rdglimg  6642  rdglim2  6649  oesuclem  6728  odi  6781  omeulem1  6784  oelim2  6797  oeoalem  6798  oeoelem  6800  limenpsi  7241  limensuci  7242  ordtypelem3  7445  ordtypelem5  7447  ordtypelem6  7448  ordtypelem7  7449  ordtypelem9  7451  r1tr  7658  r1ordg  7660  r1ord3g  7661  r1pwss  7666  r1val1  7668  rankwflemb  7675  r1elwf  7678  rankr1ai  7680  rankr1ag  7684  rankr1bg  7685  unwf  7692  rankr1clem  7702  rankr1c  7703  rankval3b  7708  rankonidlem  7710  onssr1  7713  coflim  8097  cflim3  8098  cflim2  8099  cfss  8101  cfslb  8102  cfslbn  8103  cfslb2n  8104  r1limwun  8567  inar1  8606  rdgprc  25365  limitssson  25665  limsucncmpi  26099

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-lim 4546