Theorem limord 6375

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

Syntax hints:   → wi 4   = wceq 1548   ≠ wne 2936  ∅c0 4264  ∪ cuni 4841  Ord word 6313  Lim wlim 6315

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 398  df-3an 1095  df-lim 6319

This theorem is referenced by:  limelon  6379  nlimsucg  7786  ordzsl  7789  limsuc  7793  limsssuc  7794  limomss  7815  trom  7819  limom  7826  tfr2b  8329  rdgsucg  8356  rdglimg  8358  rdglim2  8365  1ellim  8427  2ellim  8428  oesuclem  8454  odi  8508  omeulem1  8511  oelim2  8525  oeoalem  8526  oeoelem  8528  limenpsi  9084  limensuci  9085  ordtypelem3  9429  ordtypelem5  9431  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  r1tr  9695  r1ordg  9697  r1ord3g  9698  r1pwss  9703  r1val1  9705  rankwflemb  9712  r1elwf  9715  rankr1ai  9717  rankr1ag  9721  rankr1bg  9722  unwf  9729  rankr1clem  9739  rankr1c  9740  rankval3b  9745  rankonidlem  9747  onssr1  9750  coflim  10178  cflim3  10179  cflim2  10180  cfss  10182  cfslb  10183  cfslbn  10184  cfslb2n  10185  r1limwun  10654  inar1  10693  oldlim  27901  rankfilimbi  35297  rankfilimb  35298  r1filimi  35299  rdgprc  36035  limsucncmpi  36688  limexissup  43741  limexissupab  43743  oaltublim  43750  omord2lim  43760  dflim5  43789  grur1cld  44691