Theorem limord 6368

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925  ∅c0 4284  ∪ cuni 4858  Ord word 6306  Lim wlim 6308

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 6312

This theorem is referenced by:  limelon  6372  nlimsucg  7775  ordzsl  7778  limsuc  7782  limsssuc  7783  limomss  7804  trom  7808  limom  7815  tfr2b  8318  rdgsucg  8345  rdglimg  8347  rdglim2  8354  1ellim  8416  2ellim  8417  oesuclem  8443  odi  8497  omeulem1  8500  oelim2  8513  oeoalem  8514  oeoelem  8516  limenpsi  9069  limensuci  9070  ordtypelem3  9412  ordtypelem5  9414  ordtypelem6  9415  ordtypelem7  9416  ordtypelem9  9418  r1tr  9672  r1ordg  9674  r1ord3g  9675  r1pwss  9680  r1val1  9682  rankwflemb  9689  r1elwf  9692  rankr1ai  9694  rankr1ag  9698  rankr1bg  9699  unwf  9706  rankr1clem  9716  rankr1c  9717  rankval3b  9722  rankonidlem  9724  onssr1  9727  coflim  10155  cflim3  10156  cflim2  10157  cfss  10159  cfslb  10160  cfslbn  10161  cfslb2n  10162  r1limwun  10630  inar1  10669  oldlim  27803  rdgprc  35788  limsucncmpi  36439  limexissup  43274  limexissupab  43276  oaltublim  43283  omord2lim  43293  dflim5  43322  grur1cld  44225