Theorem limord 6393

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925  ∅c0 4296  ∪ cuni 4871  Ord word 6331  Lim wlim 6333

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 6337

This theorem is referenced by:  limelon  6397  nlimsucg  7818  ordzsl  7821  limsuc  7825  limsssuc  7826  limomss  7847  trom  7851  limom  7858  tfr2b  8364  rdgsucg  8391  rdglimg  8393  rdglim2  8400  1ellim  8462  2ellim  8463  oesuclem  8489  odi  8543  omeulem1  8546  oelim2  8559  oeoalem  8560  oeoelem  8562  limenpsi  9116  limensuci  9117  ordtypelem3  9473  ordtypelem5  9475  ordtypelem6  9476  ordtypelem7  9477  ordtypelem9  9479  r1tr  9729  r1ordg  9731  r1ord3g  9732  r1pwss  9737  r1val1  9739  rankwflemb  9746  r1elwf  9749  rankr1ai  9751  rankr1ag  9755  rankr1bg  9756  unwf  9763  rankr1clem  9773  rankr1c  9774  rankval3b  9779  rankonidlem  9781  onssr1  9784  coflim  10214  cflim3  10215  cflim2  10216  cfss  10218  cfslb  10219  cfslbn  10220  cfslb2n  10221  r1limwun  10689  inar1  10728  oldlim  27798  rdgprc  35782  limsucncmpi  36433  limexissup  43270  limexissupab  43272  oaltublim  43279  omord2lim  43289  dflim5  43318  grur1cld  44221