Theorem limord 6443

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2939  ∅c0 4332  ∪ cuni 4906  Ord word 6382  Lim wlim 6384

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 6388

This theorem is referenced by:  0ellim  6446  limelon  6447  nlimsucg  7864  ordzsl  7867  limsuc  7871  limsssuc  7872  limomss  7893  trom  7897  limom  7904  tfr2b  8437  rdgsucg  8464  rdglimg  8466  rdglim2  8473  1ellim  8537  2ellim  8538  oesuclem  8564  odi  8618  omeulem1  8621  oelim2  8634  oeoalem  8635  oeoelem  8637  limenpsi  9193  limensuci  9194  ordtypelem3  9561  ordtypelem5  9563  ordtypelem6  9564  ordtypelem7  9565  ordtypelem9  9567  r1tr  9817  r1ordg  9819  r1ord3g  9820  r1pwss  9825  r1val1  9827  rankwflemb  9834  r1elwf  9837  rankr1ai  9839  rankr1ag  9843  rankr1bg  9844  unwf  9851  rankr1clem  9861  rankr1c  9862  rankval3b  9867  rankonidlem  9869  onssr1  9872  coflim  10302  cflim3  10303  cflim2  10304  cfss  10306  cfslb  10307  cfslbn  10308  cfslb2n  10309  r1limwun  10777  inar1  10816  oldlim  27926  rdgprc  35796  limsucncmpi  36447  limexissup  43299  limexissupab  43301  oaltublim  43308  omord2lim  43318  dflim5  43347  grur1cld  44256