Theorem limord 6439

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2959  ∅c0 4281  ∪ cuni 4870  Ord word 6376  Lim wlim 6378

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 6382

This theorem is used by:  limelon  6443  nlimsucg  7874  ordzsl  7877  limsuc  7881  limsssuc  7882  limomss  7903  trom  7907  limom  7914  tfr2b  8429  rdgsucg  8456  rdglimg  8458  rdglim2  8465  1ellim  8531  2ellim  8532  oesuclem  8558  odi  8612  omeulem1  8615  oelim2  8629  oeoalem  8630  oeoelem  8632  limenpsi  9196  limensuci  9197  ordtypelem3  9538  ordtypelem5  9540  ordtypelem6  9541  ordtypelem7  9542  ordtypelem9  9544  rnr1  9798  r1tr  9807  r1ordg  9809  r1ord3g  9810  r1pwss  9815  r1val1  9817  rankwflembOLD  9825  r1elwf  9828  rankr1ai  9830  rankr1ag  9834  rankr1bg  9835  unwf  9842  rankr1clem  9853  rankr1c  9854  rankval3b  9860  rankonidlem  9862  onssr1  9867  rankfilimbi  9926  r1filimi  9927  coflim  10363  cflim3  10364  cflim2  10365  cfss  10367  cfslb  10368  cfslbn  10369  cfslb2n  10370  r1limwun  10845  inar1  10884  oldlim  28300  rankfilimb  35809  rdgprc  36733  limsucncmpi  37410  limexissup  44473  limexissupab  44475  oaltublim  44482  omord2lim  44492  dflim5  44521  grur1cld  45420