Theorem limord 6379

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4286  ∪ cuni 4864  Ord word 6317  Lim wlim 6319

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 6323

This theorem is referenced by:  limelon  6383  nlimsucg  7786  ordzsl  7789  limsuc  7793  limsssuc  7794  limomss  7815  trom  7819  limom  7826  tfr2b  8329  rdgsucg  8356  rdglimg  8358  rdglim2  8365  1ellim  8427  2ellim  8428  oesuclem  8454  odi  8508  omeulem1  8511  oelim2  8525  oeoalem  8526  oeoelem  8528  limenpsi  9084  limensuci  9085  ordtypelem3  9429  ordtypelem5  9431  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  r1tr  9692  r1ordg  9694  r1ord3g  9695  r1pwss  9700  r1val1  9702  rankwflemb  9709  r1elwf  9712  rankr1ai  9714  rankr1ag  9718  rankr1bg  9719  unwf  9726  rankr1clem  9736  rankr1c  9737  rankval3b  9742  rankonidlem  9744  onssr1  9747  coflim  10175  cflim3  10176  cflim2  10177  cfss  10179  cfslb  10180  cfslbn  10181  cfslb2n  10182  r1limwun  10651  inar1  10690  oldlim  27887  rankfilimbi  35259  rankfilimb  35260  r1filimi  35261  rdgprc  35988  limsucncmpi  36641  limexissup  43590  limexissupab  43592  oaltublim  43599  omord2lim  43609  dflim5  43638  grur1cld  44540