Theorem limord 6409

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 6353	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp1bi 1159	1 ⊢ (Lim 𝐴 → Ord 𝐴)

Syntax hints:   → wi 4   = wceq 1562   ≠ wne 2959  ∅c0 4287  ∪ cuni 4867  Ord word 6347  Lim wlim 6349

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 209  df-an 400  df-3an 1101  df-lim 6353

This theorem is referenced by:  limelon  6413  nlimsucg  7824  ordzsl  7827  limsuc  7831  limsssuc  7832  limomss  7853  trom  7857  limom  7864  tfr2b  8369  rdgsucg  8396  rdglimg  8398  rdglim2  8405  1ellim  8469  2ellim  8470  oesuclem  8496  odi  8550  omeulem1  8553  oelim2  8567  oeoalem  8568  oeoelem  8570  limenpsi  9126  limensuci  9127  ordtypelem3  9470  ordtypelem5  9472  ordtypelem6  9473  ordtypelem7  9474  ordtypelem9  9476  r1tr  9736  r1ordg  9738  r1ord3g  9739  r1pwss  9744  r1val1  9746  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankr1ag  9762  rankr1bg  9763  unwf  9770  rankr1clem  9780  rankr1c  9781  rankval3b  9786  rankonidlem  9788  onssr1  9791  coflim  10220  cflim3  10221  cflim2  10222  cfss  10224  cfslb  10225  cfslbn  10226  cfslb2n  10227  r1limwun  10696  inar1  10735  oldlim  27982  rankfilimbi  35401  rankfilimb  35402  r1filimi  35403  rdgprc  36147  limsucncmpi  36810  limexissup  43863  limexissupab  43865  oaltublim  43872  omord2lim  43882  dflim5  43911  grur1cld  44813