Theorem limord 6225

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2934  ∅c0 4209  ∪ cuni 4793  Ord word 6165  Lim wlim 6167

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 210  df-an 400  df-3an 1090  df-lim 6171

This theorem is referenced by:  0ellim  6228  limelon  6229  nlimsucg  7570  ordzsl  7573  limsuc  7577  limsssuc  7578  limomss  7598  ordom  7602  limom  7608  tfr2b  8054  rdgsucg  8081  rdglimg  8083  rdglim2  8090  oesuclem  8174  odi  8229  omeulem1  8232  oelim2  8245  oeoalem  8246  oeoelem  8248  limenpsi  8735  limensuci  8736  ordtypelem3  9050  ordtypelem5  9052  ordtypelem6  9053  ordtypelem7  9054  ordtypelem9  9056  r1tr  9271  r1ordg  9273  r1ord3g  9274  r1pwss  9279  r1val1  9281  rankwflemb  9288  r1elwf  9291  rankr1ai  9293  rankr1ag  9297  rankr1bg  9298  unwf  9305  rankr1clem  9315  rankr1c  9316  rankval3b  9321  rankonidlem  9323  onssr1  9326  coflim  9754  cflim3  9755  cflim2  9756  cfss  9758  cfslb  9759  cfslbn  9760  cfslb2n  9761  r1limwun  10229  inar1  10268  rdgprc  33334  oldlim  33699  limsucncmpi  34264  grur1cld  41376