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

Theorem limord 6249
 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 6195 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1141 1 (Lim 𝐴 → Ord 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1533   ≠ wne 3016  ∅c0 4290  ∪ cuni 4837  Ord word 6189  Lim wlim 6191 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 209  df-an 399  df-3an 1085  df-lim 6195 This theorem is referenced by:  0ellim  6252  limelon  6253  nlimsucg  7556  ordzsl  7559  limsuc  7563  limsssuc  7564  limomss  7584  ordom  7588  limom  7594  tfr2b  8031  rdgsucg  8058  rdglimg  8060  rdglim2  8067  oesuclem  8149  odi  8204  omeulem1  8207  oelim2  8220  oeoalem  8221  oeoelem  8223  limenpsi  8691  limensuci  8692  ordtypelem3  8983  ordtypelem5  8985  ordtypelem6  8986  ordtypelem7  8987  ordtypelem9  8989  r1tr  9204  r1ordg  9206  r1ord3g  9207  r1pwss  9212  r1val1  9214  rankwflemb  9221  r1elwf  9224  rankr1ai  9226  rankr1ag  9230  rankr1bg  9231  unwf  9238  rankr1clem  9248  rankr1c  9249  rankval3b  9254  rankonidlem  9256  onssr1  9259  coflim  9682  cflim3  9683  cflim2  9684  cfss  9686  cfslb  9687  cfslbn  9688  cfslb2n  9689  r1limwun  10157  inar1  10196  rdgprc  33039  limsucncmpi  33793  grur1cld  40568
 Copyright terms: Public domain W3C validator