Theorem limord 6388

Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limord	⊢ (Lim 𝐴 → Ord 𝐴)

Proof of Theorem limord

Step	Hyp	Ref	Expression
1		df-lim 6332	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp1bi 1146	1 ⊢ (Lim 𝐴 → Ord 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4287  ∪ cuni 4865  Ord word 6326  Lim wlim 6328

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 207  df-an 396  df-3an 1089  df-lim 6332

This theorem is referenced by:  limelon  6392  nlimsucg  7796  ordzsl  7799  limsuc  7803  limsssuc  7804  limomss  7825  trom  7829  limom  7836  tfr2b  8339  rdgsucg  8366  rdglimg  8368  rdglim2  8375  1ellim  8437  2ellim  8438  oesuclem  8464  odi  8518  omeulem1  8521  oelim2  8535  oeoalem  8536  oeoelem  8538  limenpsi  9094  limensuci  9095  ordtypelem3  9439  ordtypelem5  9441  ordtypelem6  9442  ordtypelem7  9443  ordtypelem9  9445  r1tr  9702  r1ordg  9704  r1ord3g  9705  r1pwss  9710  r1val1  9712  rankwflemb  9719  r1elwf  9722  rankr1ai  9724  rankr1ag  9728  rankr1bg  9729  unwf  9736  rankr1clem  9746  rankr1c  9747  rankval3b  9752  rankonidlem  9754  onssr1  9757  coflim  10185  cflim3  10186  cflim2  10187  cfss  10189  cfslb  10190  cfslbn  10191  cfslb2n  10192  r1limwun  10661  inar1  10700  oldlim  27900  rankfilimbi  35284  rankfilimb  35285  r1filimi  35286  rdgprc  36014  limsucncmpi  36667  limexissup  43667  limexissupab  43669  oaltublim  43676  omord2lim  43686  dflim5  43715  grur1cld  44617