Theorem limord 5784

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

Syntax hints:   → wi 4   = wceq 1483   ≠ wne 2794  ∅c0 3915  ∪ cuni 4436  Ord word 5722  Lim wlim 5724

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 197  df-an 386  df-3an 1039  df-lim 5728

This theorem is referenced by:  0ellim  5787  limelon  5788  nlimsucg  7042  ordzsl  7045  limsuc  7049  limsssuc  7050  limomss  7070  ordom  7074  limom  7080  tfr2b  7492  rdgsucg  7519  rdglimg  7521  rdglim2  7528  oesuclem  7605  odi  7659  omeulem1  7662  oelim2  7675  oeoalem  7676  oeoelem  7678  limenpsi  8135  limensuci  8136  ordtypelem3  8425  ordtypelem5  8427  ordtypelem6  8428  ordtypelem7  8429  ordtypelem9  8431  r1tr  8639  r1ordg  8641  r1ord3g  8642  r1pwss  8647  r1val1  8649  rankwflemb  8656  r1elwf  8659  rankr1ai  8661  rankr1ag  8665  rankr1bg  8666  unwf  8673  rankr1clem  8683  rankr1c  8684  rankval3b  8689  rankonidlem  8691  onssr1  8694  coflim  9083  cflim3  9084  cflim2  9085  cfss  9087  cfslb  9088  cfslbn  9089  cfslb2n  9090  r1limwun  9558  inar1  9597  rdgprc  31700  limsucncmpi  32444