Theorem limord 6396

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926  ∅c0 4299  ∪ cuni 4874  Ord word 6334  Lim wlim 6336

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 1088  df-lim 6340

This theorem is referenced by:  limelon  6400  nlimsucg  7821  ordzsl  7824  limsuc  7828  limsssuc  7829  limomss  7850  trom  7854  limom  7861  tfr2b  8367  rdgsucg  8394  rdglimg  8396  rdglim2  8403  1ellim  8465  2ellim  8466  oesuclem  8492  odi  8546  omeulem1  8549  oelim2  8562  oeoalem  8563  oeoelem  8565  limenpsi  9122  limensuci  9123  ordtypelem3  9480  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  r1tr  9736  r1ordg  9738  r1ord3g  9739  r1pwss  9744  r1val1  9746  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankr1ag  9762  rankr1bg  9763  unwf  9770  rankr1clem  9780  rankr1c  9781  rankval3b  9786  rankonidlem  9788  onssr1  9791  coflim  10221  cflim3  10222  cflim2  10223  cfss  10225  cfslb  10226  cfslbn  10227  cfslb2n  10228  r1limwun  10696  inar1  10735  oldlim  27805  rdgprc  35789  limsucncmpi  36440  limexissup  43277  limexissupab  43279  oaltublim  43286  omord2lim  43296  dflim5  43325  grur1cld  44228