Theorem limord 6422

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2957  ∅c0 4285  ∪ cuni 4871  Ord word 6359  Lim wlim 6361

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 401  df-3an 1104  df-lim 6365

This theorem is used by:  limelon  6426  nlimsucg  7836  ordzsl  7839  limsuc  7843  limsssuc  7844  limomss  7865  trom  7869  limom  7876  tfr2b  8381  rdgsucg  8408  rdglimg  8410  rdglim2  8417  1ellim  8481  2ellim  8482  oesuclem  8508  odi  8562  omeulem1  8565  oelim2  8579  oeoalem  8580  oeoelem  8582  limenpsi  9138  limensuci  9139  ordtypelem3  9480  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  r1tr  9746  r1ordg  9748  r1ord3g  9749  r1pwss  9754  r1val1  9756  rankwflemb  9763  r1elwf  9766  rankr1ai  9768  rankr1ag  9772  rankr1bg  9773  unwf  9780  rankr1clem  9790  rankr1c  9791  rankval3b  9796  rankonidlem  9798  onssr1  9801  coflim  10251  cflim3  10252  cflim2  10253  cfss  10255  cfslb  10256  cfslbn  10257  cfslb2n  10258  r1limwun  10727  inar1  10766  oldlim  28091  rankfilimbi  35504  rankfilimb  35505  r1filimi  35506  rdgprc  36292  limsucncmpi  36984  limexissup  44036  limexissupab  44038  oaltublim  44045  omord2lim  44055  dflim5  44084  grur1cld  44984