Theorem limord 6218

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

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987  ∅c0 4243  ∪ cuni 4800  Ord word 6158  Lim wlim 6160

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 210  df-an 400  df-3an 1086  df-lim 6164

This theorem is referenced by:  0ellim  6221  limelon  6222  nlimsucg  7537  ordzsl  7540  limsuc  7544  limsssuc  7545  limomss  7565  ordom  7569  limom  7575  tfr2b  8015  rdgsucg  8042  rdglimg  8044  rdglim2  8051  oesuclem  8133  odi  8188  omeulem1  8191  oelim2  8204  oeoalem  8205  oeoelem  8207  limenpsi  8676  limensuci  8677  ordtypelem3  8968  ordtypelem5  8970  ordtypelem6  8971  ordtypelem7  8972  ordtypelem9  8974  r1tr  9189  r1ordg  9191  r1ord3g  9192  r1pwss  9197  r1val1  9199  rankwflemb  9206  r1elwf  9209  rankr1ai  9211  rankr1ag  9215  rankr1bg  9216  unwf  9223  rankr1clem  9233  rankr1c  9234  rankval3b  9239  rankonidlem  9241  onssr1  9244  coflim  9672  cflim3  9673  cflim2  9674  cfss  9676  cfslb  9677  cfslbn  9678  cfslb2n  9679  r1limwun  10147  inar1  10186  rdgprc  33152  limsucncmpi  33906  grur1cld  40940