Theorem limord 6381

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925  ∅c0 4292  ∪ cuni 4867  Ord word 6319  Lim wlim 6321

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 207  df-an 396  df-3an 1088  df-lim 6325

This theorem is referenced by:  limelon  6385  nlimsucg  7798  ordzsl  7801  limsuc  7805  limsssuc  7806  limomss  7827  trom  7831  limom  7838  tfr2b  8341  rdgsucg  8368  rdglimg  8370  rdglim2  8377  1ellim  8439  2ellim  8440  oesuclem  8466  odi  8520  omeulem1  8523  oelim2  8536  oeoalem  8537  oeoelem  8539  limenpsi  9093  limensuci  9094  ordtypelem3  9449  ordtypelem5  9451  ordtypelem6  9452  ordtypelem7  9453  ordtypelem9  9455  r1tr  9705  r1ordg  9707  r1ord3g  9708  r1pwss  9713  r1val1  9715  rankwflemb  9722  r1elwf  9725  rankr1ai  9727  rankr1ag  9731  rankr1bg  9732  unwf  9739  rankr1clem  9749  rankr1c  9750  rankval3b  9755  rankonidlem  9757  onssr1  9760  coflim  10190  cflim3  10191  cflim2  10192  cfss  10194  cfslb  10195  cfslbn  10196  cfslb2n  10197  r1limwun  10665  inar1  10704  oldlim  27836  rdgprc  35775  limsucncmpi  36426  limexissup  43263  limexissupab  43265  oaltublim  43272  omord2lim  43282  dflim5  43311  grur1cld  44214