Theorem limord 6384

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2932  ∅c0 4273  ∪ cuni 4850  Ord word 6322  Lim wlim 6324

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 6328

This theorem is referenced by:  limelon  6388  nlimsucg  7793  ordzsl  7796  limsuc  7800  limsssuc  7801  limomss  7822  trom  7826  limom  7833  tfr2b  8335  rdgsucg  8362  rdglimg  8364  rdglim2  8371  1ellim  8433  2ellim  8434  oesuclem  8460  odi  8514  omeulem1  8517  oelim2  8531  oeoalem  8532  oeoelem  8534  limenpsi  9090  limensuci  9091  ordtypelem3  9435  ordtypelem5  9437  ordtypelem6  9438  ordtypelem7  9439  ordtypelem9  9441  r1tr  9700  r1ordg  9702  r1ord3g  9703  r1pwss  9708  r1val1  9710  rankwflemb  9717  r1elwf  9720  rankr1ai  9722  rankr1ag  9726  rankr1bg  9727  unwf  9734  rankr1clem  9744  rankr1c  9745  rankval3b  9750  rankonidlem  9752  onssr1  9755  coflim  10183  cflim3  10184  cflim2  10185  cfss  10187  cfslb  10188  cfslbn  10189  cfslb2n  10190  r1limwun  10659  inar1  10698  oldlim  27879  rankfilimbi  35244  rankfilimb  35245  r1filimi  35246  rdgprc  35974  limsucncmpi  36627  limexissup  43709  limexissupab  43711  oaltublim  43718  omord2lim  43728  dflim5  43757  grur1cld  44659