Theorem limord 6414

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2955  ∅c0 4279  ∪ cuni 4867  Ord word 6351  Lim wlim 6353

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-lim 6357

This theorem is used by:  limelon  6418  nlimsucg  7837  ordzsl  7840  limsuc  7844  limsssuc  7845  limomss  7866  trom  7870  limom  7877  tfr2b  8383  rdgsucg  8410  rdglimg  8412  rdglim2  8419  1ellim  8485  2ellim  8486  oesuclem  8512  odi  8566  omeulem1  8569  oelim2  8583  oeoalem  8584  oeoelem  8586  limenpsi  9150  limensuci  9151  ordtypelem3  9492  ordtypelem5  9494  ordtypelem6  9495  ordtypelem7  9496  ordtypelem9  9498  r1tr  9758  r1ordg  9760  r1ord3g  9761  r1pwss  9766  r1val1  9768  rankwflemb  9775  r1elwf  9778  rankr1ai  9780  rankr1ag  9784  rankr1bg  9785  unwf  9792  rankr1clem  9802  rankr1c  9803  rankval3b  9808  rankonidlem  9810  onssr1  9813  coflim  10296  cflim3  10297  cflim2  10298  cfss  10300  cfslb  10301  cfslbn  10302  cfslb2n  10303  r1limwun  10778  inar1  10817  oldlim  28192  rankfilimbi  35650  rankfilimb  35651  r1filimi  35652  rdgprc  36472  limsucncmpi  37149  limexissup  44220  limexissupab  44222  oaltublim  44229  omord2lim  44239  dflim5  44268  grur1cld  45168