Theorem limord 6424

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2939  ∅c0 4322  ∪ cuni 4908  Ord word 6363  Lim wlim 6365

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 206  df-an 396  df-3an 1088  df-lim 6369

This theorem is referenced by:  0ellim  6427  limelon  6428  nlimsucg  7835  ordzsl  7838  limsuc  7842  limsssuc  7843  limomss  7864  trom  7868  limom  7875  tfr2b  8402  rdgsucg  8429  rdglimg  8431  rdglim2  8438  1ellim  8504  2ellim  8505  oesuclem  8531  odi  8585  omeulem1  8588  oelim2  8601  oeoalem  8602  oeoelem  8604  limenpsi  9158  limensuci  9159  ordtypelem3  9521  ordtypelem5  9523  ordtypelem6  9524  ordtypelem7  9525  ordtypelem9  9527  r1tr  9777  r1ordg  9779  r1ord3g  9780  r1pwss  9785  r1val1  9787  rankwflemb  9794  r1elwf  9797  rankr1ai  9799  rankr1ag  9803  rankr1bg  9804  unwf  9811  rankr1clem  9821  rankr1c  9822  rankval3b  9827  rankonidlem  9829  onssr1  9832  coflim  10262  cflim3  10263  cflim2  10264  cfss  10266  cfslb  10267  cfslbn  10268  cfslb2n  10269  r1limwun  10737  inar1  10776  oldlim  27727  rdgprc  35237  limsucncmpi  35796  limexissup  42496  limexissupab  42498  oaltublim  42505  omord2lim  42515  dflim5  42544  grur1cld  43456