Theorem limord 6425

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941  ∅c0 4323  ∪ cuni 4909  Ord word 6364  Lim wlim 6366

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 206  df-an 398  df-3an 1090  df-lim 6370

This theorem is referenced by:  0ellim  6428  limelon  6429  nlimsucg  7831  ordzsl  7834  limsuc  7838  limsssuc  7839  limomss  7860  trom  7864  limom  7871  tfr2b  8396  rdgsucg  8423  rdglimg  8425  rdglim2  8432  1ellim  8498  2ellim  8499  oesuclem  8525  odi  8579  omeulem1  8582  oelim2  8595  oeoalem  8596  oeoelem  8598  limenpsi  9152  limensuci  9153  ordtypelem3  9515  ordtypelem5  9517  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  r1tr  9771  r1ordg  9773  r1ord3g  9774  r1pwss  9779  r1val1  9781  rankwflemb  9788  r1elwf  9791  rankr1ai  9793  rankr1ag  9797  rankr1bg  9798  unwf  9805  rankr1clem  9815  rankr1c  9816  rankval3b  9821  rankonidlem  9823  onssr1  9826  coflim  10256  cflim3  10257  cflim2  10258  cfss  10260  cfslb  10261  cfslbn  10262  cfslb2n  10263  r1limwun  10731  inar1  10770  oldlim  27381  rdgprc  34766  limsucncmpi  35330  limexissup  42031  limexissupab  42033  oaltublim  42040  omord2lim  42050  dflim5  42079  grur1cld  42991