Theorem limord 6455

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946  ∅c0 4352  ∪ cuni 4931  Ord word 6394  Lim wlim 6396

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 1089  df-lim 6400

This theorem is referenced by:  0ellim  6458  limelon  6459  nlimsucg  7879  ordzsl  7882  limsuc  7886  limsssuc  7887  limomss  7908  trom  7912  limom  7919  tfr2b  8452  rdgsucg  8479  rdglimg  8481  rdglim2  8488  1ellim  8554  2ellim  8555  oesuclem  8581  odi  8635  omeulem1  8638  oelim2  8651  oeoalem  8652  oeoelem  8654  limenpsi  9218  limensuci  9219  ordtypelem3  9589  ordtypelem5  9591  ordtypelem6  9592  ordtypelem7  9593  ordtypelem9  9595  r1tr  9845  r1ordg  9847  r1ord3g  9848  r1pwss  9853  r1val1  9855  rankwflemb  9862  r1elwf  9865  rankr1ai  9867  rankr1ag  9871  rankr1bg  9872  unwf  9879  rankr1clem  9889  rankr1c  9890  rankval3b  9895  rankonidlem  9897  onssr1  9900  coflim  10330  cflim3  10331  cflim2  10332  cfss  10334  cfslb  10335  cfslbn  10336  cfslb2n  10337  r1limwun  10805  inar1  10844  oldlim  27943  rdgprc  35758  limsucncmpi  36411  limexissup  43243  limexissupab  43245  oaltublim  43252  omord2lim  43262  dflim5  43291  grur1cld  44201