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

Theorem limord 6443
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 6388 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1145 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wne 2939  c0 4332   cuni 4906  Ord word 6382  Lim wlim 6384
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 1088  df-lim 6388
This theorem is referenced by:  0ellim  6446  limelon  6447  nlimsucg  7864  ordzsl  7867  limsuc  7871  limsssuc  7872  limomss  7893  trom  7897  limom  7904  tfr2b  8437  rdgsucg  8464  rdglimg  8466  rdglim2  8473  1ellim  8537  2ellim  8538  oesuclem  8564  odi  8618  omeulem1  8621  oelim2  8634  oeoalem  8635  oeoelem  8637  limenpsi  9193  limensuci  9194  ordtypelem3  9561  ordtypelem5  9563  ordtypelem6  9564  ordtypelem7  9565  ordtypelem9  9567  r1tr  9817  r1ordg  9819  r1ord3g  9820  r1pwss  9825  r1val1  9827  rankwflemb  9834  r1elwf  9837  rankr1ai  9839  rankr1ag  9843  rankr1bg  9844  unwf  9851  rankr1clem  9861  rankr1c  9862  rankval3b  9867  rankonidlem  9869  onssr1  9872  coflim  10302  cflim3  10303  cflim2  10304  cfss  10306  cfslb  10307  cfslbn  10308  cfslb2n  10309  r1limwun  10777  inar1  10816  oldlim  27926  rdgprc  35796  limsucncmpi  36447  limexissup  43299  limexissupab  43301  oaltublim  43308  omord2lim  43318  dflim5  43347  grur1cld  44256
  Copyright terms: Public domain W3C validator