Theorem limord 6418

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2933  ∅c0 4313  ∪ cuni 4888  Ord word 6356  Lim wlim 6358

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 6362

This theorem is referenced by:  0ellim  6421  limelon  6422  nlimsucg  7842  ordzsl  7845  limsuc  7849  limsssuc  7850  limomss  7871  trom  7875  limom  7882  tfr2b  8415  rdgsucg  8442  rdglimg  8444  rdglim2  8451  1ellim  8515  2ellim  8516  oesuclem  8542  odi  8596  omeulem1  8599  oelim2  8612  oeoalem  8613  oeoelem  8615  limenpsi  9171  limensuci  9172  ordtypelem3  9539  ordtypelem5  9541  ordtypelem6  9542  ordtypelem7  9543  ordtypelem9  9545  r1tr  9795  r1ordg  9797  r1ord3g  9798  r1pwss  9803  r1val1  9805  rankwflemb  9812  r1elwf  9815  rankr1ai  9817  rankr1ag  9821  rankr1bg  9822  unwf  9829  rankr1clem  9839  rankr1c  9840  rankval3b  9845  rankonidlem  9847  onssr1  9850  coflim  10280  cflim3  10281  cflim2  10282  cfss  10284  cfslb  10285  cfslbn  10286  cfslb2n  10287  r1limwun  10755  inar1  10794  oldlim  27855  rdgprc  35817  limsucncmpi  36468  limexissup  43272  limexissupab  43274  oaltublim  43281  omord2lim  43291  dflim5  43320  grur1cld  44223