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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955  ∅c0 4278  ∪ cuni 4866  Ord word 6361  Lim wlim 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-lim 6367

This theorem is used by:  limelon  6428  nlimsucg  7853  ordzsl  7856  limsuc  7860  limsssuc  7861  limomss  7882  trom  7886  limom  7893  tfr2b  8404  rdgsucg  8431  rdglimg  8433  rdglim2  8440  1ellim  8506  2ellim  8507  oesuclem  8533  odi  8587  omeulem1  8590  oelim2  8604  oeoalem  8605  oeoelem  8607  limenpsi  9171  limensuci  9172  ordtypelem3  9514  ordtypelem5  9516  ordtypelem6  9517  ordtypelem7  9518  ordtypelem9  9520  rnr1  9774  r1tr  9783  r1ordg  9785  r1ord3g  9786  r1pwss  9791  r1val1  9793  rankwflembOLD  9801  r1elwf  9804  rankr1ai  9806  rankr1ag  9810  rankr1bg  9811  unwf  9818  rankr1clem  9829  rankr1c  9830  rankval3b  9836  rankonidlem  9838  onssr1  9843  rankfilimbi  9902  r1filimi  9903  coflim  10339  cflim3  10340  cflim2  10341  cfss  10343  cfslb  10344  cfslbn  10345  cfslb2n  10346  r1limwun  10821  inar1  10860  oldlim  28273  rankfilimb  35728  rdgprc  36556  limsucncmpi  37233  limexissup  44283  limexissupab  44285  oaltublim  44292  omord2lim  44302  dflim5  44331  grur1cld  45230