Theorem limord 6423

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2957  ∅c0 4282  ∪ cuni 4870  Ord word 6360  Lim wlim 6362

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 6366

This theorem is used by:  limelon  6427  nlimsucg  7841  ordzsl  7844  limsuc  7848  limsssuc  7849  limomss  7870  trom  7874  limom  7881  tfr2b  8388  rdgsucg  8415  rdglimg  8417  rdglim2  8424  1ellim  8488  2ellim  8489  oesuclem  8515  odi  8569  omeulem1  8572  oelim2  8586  oeoalem  8587  oeoelem  8589  limenpsi  9153  limensuci  9154  ordtypelem3  9495  ordtypelem5  9497  ordtypelem6  9498  ordtypelem7  9499  ordtypelem9  9501  r1tr  9761  r1ordg  9763  r1ord3g  9764  r1pwss  9769  r1val1  9771  rankwflemb  9778  r1elwf  9781  rankr1ai  9783  rankr1ag  9787  rankr1bg  9788  unwf  9795  rankr1clem  9805  rankr1c  9806  rankval3b  9811  rankonidlem  9813  onssr1  9816  coflim  10266  cflim3  10267  cflim2  10268  cfss  10270  cfslb  10271  cfslbn  10272  cfslb2n  10273  r1limwun  10748  inar1  10787  oldlim  28150  rankfilimbi  35596  rankfilimb  35597  r1filimi  35598  rdgprc  36358  limsucncmpi  37051  limexissup  44109  limexissupab  44111  oaltublim  44118  omord2lim  44128  dflim5  44157  grur1cld  45057