Theorem limord 6252

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3018  ∅c0 4293  ∪ cuni 4840  Ord word 6192  Lim wlim 6194

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 209  df-an 399  df-3an 1085  df-lim 6198

This theorem is referenced by:  0ellim  6255  limelon  6256  nlimsucg  7559  ordzsl  7562  limsuc  7566  limsssuc  7567  limomss  7587  ordom  7591  limom  7597  tfr2b  8034  rdgsucg  8061  rdglimg  8063  rdglim2  8070  oesuclem  8152  odi  8207  omeulem1  8210  oelim2  8223  oeoalem  8224  oeoelem  8226  limenpsi  8694  limensuci  8695  ordtypelem3  8986  ordtypelem5  8988  ordtypelem6  8989  ordtypelem7  8990  ordtypelem9  8992  r1tr  9207  r1ordg  9209  r1ord3g  9210  r1pwss  9215  r1val1  9217  rankwflemb  9224  r1elwf  9227  rankr1ai  9229  rankr1ag  9233  rankr1bg  9234  unwf  9241  rankr1clem  9251  rankr1c  9252  rankval3b  9257  rankonidlem  9259  onssr1  9262  coflim  9685  cflim3  9686  cflim2  9687  cfss  9689  cfslb  9690  cfslbn  9691  cfslb2n  9692  r1limwun  10160  inar1  10199  rdgprc  33041  limsucncmpi  33795  grur1cld  40575