Theorem limord 6423

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964  ∅c0 4292  ∪ cuni 4874  Ord word 6360  Lim wlim 6362

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 210  df-an 401  df-3an 1103  df-lim 6366

This theorem is referenced by:  limelon  6427  nlimsucg  7838  ordzsl  7841  limsuc  7845  limsssuc  7846  limomss  7867  trom  7871  limom  7878  tfr2b  8383  rdgsucg  8410  rdglimg  8412  rdglim2  8419  1ellim  8483  2ellim  8484  oesuclem  8510  odi  8564  omeulem1  8567  oelim2  8581  oeoalem  8582  oeoelem  8584  limenpsi  9140  limensuci  9141  ordtypelem3  9482  ordtypelem5  9484  ordtypelem6  9485  ordtypelem7  9486  ordtypelem9  9488  r1tr  9748  r1ordg  9750  r1ord3g  9751  r1pwss  9756  r1val1  9758  rankwflemb  9765  r1elwf  9768  rankr1ai  9770  rankr1ag  9774  rankr1bg  9775  unwf  9782  rankr1clem  9792  rankr1c  9793  rankval3b  9798  rankonidlem  9800  onssr1  9803  coflim  10245  cflim3  10246  cflim2  10247  cfss  10249  cfslb  10250  cfslbn  10251  cfslb2n  10252  r1limwun  10721  inar1  10760  oldlim  28046  rankfilimbi  35438  rankfilimb  35439  r1filimi  35440  rdgprc  36217  limsucncmpi  36879  limexissup  43935  limexissupab  43937  oaltublim  43944  omord2lim  43954  dflim5  43983  grur1cld  44883