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  9707  r1ordg  9709  r1ord3g  9710  r1pwss  9715  r1val1  9717  rankwflemb  9724  r1elwf  9727  rankr1ai  9729  rankr1ag  9733  rankr1bg  9734  unwf  9741  rankr1clem  9751  rankr1c  9752  rankval3b  9757  rankonidlem  9759  onssr1  9762  coflim  10192  cflim3  10193  cflim2  10194  cfss  10196  cfslb  10197  cfslbn  10198  cfslb2n  10199  r1limwun  10667  inar1  10706  oldlim  27837  rdgprc  35776  limsucncmpi  36427  limexissup  43264  limexissupab  43266  oaltublim  43273  omord2lim  43283  dflim5  43312  grur1cld  44215