Theorem limord 6376

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

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

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 6320

This theorem is referenced by:  limelon  6380  nlimsucg  7784  ordzsl  7787  limsuc  7791  limsssuc  7792  limomss  7813  trom  7817  limom  7824  tfr2b  8326  rdgsucg  8353  rdglimg  8355  rdglim2  8362  1ellim  8424  2ellim  8425  oesuclem  8451  odi  8505  omeulem1  8508  oelim2  8522  oeoalem  8523  oeoelem  8525  limenpsi  9081  limensuci  9082  ordtypelem3  9426  ordtypelem5  9428  ordtypelem6  9429  ordtypelem7  9430  ordtypelem9  9432  r1tr  9689  r1ordg  9691  r1ord3g  9692  r1pwss  9697  r1val1  9699  rankwflemb  9706  r1elwf  9709  rankr1ai  9711  rankr1ag  9715  rankr1bg  9716  unwf  9723  rankr1clem  9733  rankr1c  9734  rankval3b  9739  rankonidlem  9741  onssr1  9744  coflim  10172  cflim3  10173  cflim2  10174  cfss  10176  cfslb  10177  cfslbn  10178  cfslb2n  10179  r1limwun  10648  inar1  10687  oldlim  27898  rankfilimbi  35265  rankfilimb  35266  r1filimi  35267  rdgprc  35995  limsucncmpi  36648  limexissup  43724  limexissupab  43726  oaltublim  43733  omord2lim  43743  dflim5  43772  grur1cld  44674