Theorem limord 6035

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

Syntax hints:   → wi 4   = wceq 1601   ≠ wne 2968  ∅c0 4140  ∪ cuni 4671  Ord word 5975  Lim wlim 5977

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 199  df-an 387  df-3an 1073  df-lim 5981

This theorem is referenced by:  0ellim  6038  limelon  6039  nlimsucg  7320  ordzsl  7323  limsuc  7327  limsssuc  7328  limomss  7348  ordom  7352  limom  7358  tfr2b  7775  rdgsucg  7802  rdglimg  7804  rdglim2  7811  oesuclem  7889  odi  7943  omeulem1  7946  oelim2  7959  oeoalem  7960  oeoelem  7962  limenpsi  8423  limensuci  8424  ordtypelem3  8714  ordtypelem5  8716  ordtypelem6  8717  ordtypelem7  8718  ordtypelem9  8720  r1tr  8936  r1ordg  8938  r1ord3g  8939  r1pwss  8944  r1val1  8946  rankwflemb  8953  r1elwf  8956  rankr1ai  8958  rankr1ag  8962  rankr1bg  8963  unwf  8970  rankr1clem  8980  rankr1c  8981  rankval3b  8986  rankonidlem  8988  onssr1  8991  coflim  9418  cflim3  9419  cflim2  9420  cfss  9422  cfslb  9423  cfslbn  9424  cfslb2n  9425  r1limwun  9893  inar1  9932  rdgprc  32302  limsucncmpi  33041