MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limord Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 df-lim 5981 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1136 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator