Theorem limord 6380

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4274  ∪ cuni 4851  Ord word 6318  Lim wlim 6320

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 1089  df-lim 6324

This theorem is referenced by:  limelon  6384  nlimsucg  7788  ordzsl  7791  limsuc  7795  limsssuc  7796  limomss  7817  trom  7821  limom  7828  tfr2b  8330  rdgsucg  8357  rdglimg  8359  rdglim2  8366  1ellim  8428  2ellim  8429  oesuclem  8455  odi  8509  omeulem1  8512  oelim2  8526  oeoalem  8527  oeoelem  8529  limenpsi  9085  limensuci  9086  ordtypelem3  9430  ordtypelem5  9432  ordtypelem6  9433  ordtypelem7  9434  ordtypelem9  9436  r1tr  9695  r1ordg  9697  r1ord3g  9698  r1pwss  9703  r1val1  9705  rankwflemb  9712  r1elwf  9715  rankr1ai  9717  rankr1ag  9721  rankr1bg  9722  unwf  9729  rankr1clem  9739  rankr1c  9740  rankval3b  9745  rankonidlem  9747  onssr1  9750  coflim  10178  cflim3  10179  cflim2  10180  cfss  10182  cfslb  10183  cfslbn  10184  cfslb2n  10185  r1limwun  10654  inar1  10693  oldlim  27897  rankfilimbi  35264  rankfilimb  35265  r1filimi  35266  rdgprc  35994  limsucncmpi  36647  limexissup  43733  limexissupab  43735  oaltublim  43742  omord2lim  43752  dflim5  43781  grur1cld  44683