Theorem limord 6367

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928  ∅c0 4280  ∪ cuni 4856  Ord word 6305  Lim wlim 6307

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 207  df-an 396  df-3an 1088  df-lim 6311

This theorem is referenced by:  limelon  6371  nlimsucg  7772  ordzsl  7775  limsuc  7779  limsssuc  7780  limomss  7801  trom  7805  limom  7812  tfr2b  8315  rdgsucg  8342  rdglimg  8344  rdglim2  8351  1ellim  8413  2ellim  8414  oesuclem  8440  odi  8494  omeulem1  8497  oelim2  8510  oeoalem  8511  oeoelem  8513  limenpsi  9065  limensuci  9066  ordtypelem3  9406  ordtypelem5  9408  ordtypelem6  9409  ordtypelem7  9410  ordtypelem9  9412  r1tr  9669  r1ordg  9671  r1ord3g  9672  r1pwss  9677  r1val1  9679  rankwflemb  9686  r1elwf  9689  rankr1ai  9691  rankr1ag  9695  rankr1bg  9696  unwf  9703  rankr1clem  9713  rankr1c  9714  rankval3b  9719  rankonidlem  9721  onssr1  9724  coflim  10152  cflim3  10153  cflim2  10154  cfss  10156  cfslb  10157  cfslbn  10158  cfslb2n  10159  r1limwun  10627  inar1  10666  oldlim  27832  rankfilimbi  35112  rankfilimb  35113  r1filimi  35114  rdgprc  35836  limsucncmpi  36489  limexissup  43373  limexissupab  43375  oaltublim  43382  omord2lim  43392  dflim5  43421  grur1cld  44324