Theorem limord 6446

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2938  ∅c0 4339  ∪ cuni 4912  Ord word 6385  Lim wlim 6387

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 6391

This theorem is referenced by:  0ellim  6449  limelon  6450  nlimsucg  7863  ordzsl  7866  limsuc  7870  limsssuc  7871  limomss  7892  trom  7896  limom  7903  tfr2b  8435  rdgsucg  8462  rdglimg  8464  rdglim2  8471  1ellim  8535  2ellim  8536  oesuclem  8562  odi  8616  omeulem1  8619  oelim2  8632  oeoalem  8633  oeoelem  8635  limenpsi  9191  limensuci  9192  ordtypelem3  9558  ordtypelem5  9560  ordtypelem6  9561  ordtypelem7  9562  ordtypelem9  9564  r1tr  9814  r1ordg  9816  r1ord3g  9817  r1pwss  9822  r1val1  9824  rankwflemb  9831  r1elwf  9834  rankr1ai  9836  rankr1ag  9840  rankr1bg  9841  unwf  9848  rankr1clem  9858  rankr1c  9859  rankval3b  9864  rankonidlem  9866  onssr1  9869  coflim  10299  cflim3  10300  cflim2  10301  cfss  10303  cfslb  10304  cfslbn  10305  cfslb2n  10306  r1limwun  10774  inar1  10813  oldlim  27940  rdgprc  35776  limsucncmpi  36428  limexissup  43271  limexissupab  43273  oaltublim  43280  omord2lim  43290  dflim5  43319  grur1cld  44228