Theorem limord 6245

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

Syntax hints:   → wi 4   = wceq 1533   ≠ wne 3016  ∅c0 4291  ∪ cuni 4832  Ord word 6185  Lim wlim 6187

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 209  df-an 399  df-3an 1085  df-lim 6191

This theorem is referenced by:  0ellim  6248  limelon  6249  nlimsucg  7551  ordzsl  7554  limsuc  7558  limsssuc  7559  limomss  7579  ordom  7583  limom  7589  tfr2b  8026  rdgsucg  8053  rdglimg  8055  rdglim2  8062  oesuclem  8144  odi  8199  omeulem1  8202  oelim2  8215  oeoalem  8216  oeoelem  8218  limenpsi  8686  limensuci  8687  ordtypelem3  8978  ordtypelem5  8980  ordtypelem6  8981  ordtypelem7  8982  ordtypelem9  8984  r1tr  9199  r1ordg  9201  r1ord3g  9202  r1pwss  9207  r1val1  9209  rankwflemb  9216  r1elwf  9219  rankr1ai  9221  rankr1ag  9225  rankr1bg  9226  unwf  9233  rankr1clem  9243  rankr1c  9244  rankval3b  9249  rankonidlem  9251  onssr1  9254  coflim  9677  cflim3  9678  cflim2  9679  cfss  9681  cfslb  9682  cfslbn  9683  cfslb2n  9684  r1limwun  10152  inar1  10191  rdgprc  33034  limsucncmpi  33788  grur1cld  40561