Theorem limord 6377

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2931  ∅c0 4284  ∪ cuni 4862  Ord word 6315  Lim wlim 6317

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 6321

This theorem is referenced by:  limelon  6381  nlimsucg  7784  ordzsl  7787  limsuc  7791  limsssuc  7792  limomss  7813  trom  7817  limom  7824  tfr2b  8327  rdgsucg  8354  rdglimg  8356  rdglim2  8363  1ellim  8425  2ellim  8426  oesuclem  8452  odi  8506  omeulem1  8509  oelim2  8523  oeoalem  8524  oeoelem  8526  limenpsi  9082  limensuci  9083  ordtypelem3  9427  ordtypelem5  9429  ordtypelem6  9430  ordtypelem7  9431  ordtypelem9  9433  r1tr  9690  r1ordg  9692  r1ord3g  9693  r1pwss  9698  r1val1  9700  rankwflemb  9707  r1elwf  9710  rankr1ai  9712  rankr1ag  9716  rankr1bg  9717  unwf  9724  rankr1clem  9734  rankr1c  9735  rankval3b  9740  rankonidlem  9742  onssr1  9745  coflim  10173  cflim3  10174  cflim2  10175  cfss  10177  cfslb  10178  cfslbn  10179  cfslb2n  10180  r1limwun  10649  inar1  10688  oldlim  27867  rankfilimbi  35236  rankfilimb  35237  r1filimi  35238  rdgprc  35965  limsucncmpi  36618  limexissup  43560  limexissupab  43562  oaltublim  43569  omord2lim  43579  dflim5  43608  grur1cld  44510