Theorem limord 6310

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2942  ∅c0 4253  ∪ cuni 4836  Ord word 6250  Lim wlim 6252

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 206  df-an 396  df-3an 1087  df-lim 6256

This theorem is referenced by:  0ellim  6313  limelon  6314  nlimsucg  7664  ordzsl  7667  limsuc  7671  limsssuc  7672  limomss  7692  trom  7696  limom  7703  tfr2b  8198  rdgsucg  8225  rdglimg  8227  rdglim2  8234  oesuclem  8317  odi  8372  omeulem1  8375  oelim2  8388  oeoalem  8389  oeoelem  8391  limenpsi  8888  limensuci  8889  ordtypelem3  9209  ordtypelem5  9211  ordtypelem6  9212  ordtypelem7  9213  ordtypelem9  9215  r1tr  9465  r1ordg  9467  r1ord3g  9468  r1pwss  9473  r1val1  9475  rankwflemb  9482  r1elwf  9485  rankr1ai  9487  rankr1ag  9491  rankr1bg  9492  unwf  9499  rankr1clem  9509  rankr1c  9510  rankval3b  9515  rankonidlem  9517  onssr1  9520  coflim  9948  cflim3  9949  cflim2  9950  cfss  9952  cfslb  9953  cfslbn  9954  cfslb2n  9955  r1limwun  10423  inar1  10462  rdgprc  33676  oldlim  33996  limsucncmpi  34561  grur1cld  41739