Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sucidg Structured version   Unicode version

Theorem sucidg 4965
 Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
Assertion
Ref Expression
sucidg

Proof of Theorem sucidg
StepHypRef Expression
1 eqid 2457 . . 3
21olci 391 . 2
3 elsucg 4954 . 2
42, 3mpbiri 233 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 368   wceq 1395   wcel 1819   csuc 4889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-suc 4893 This theorem is referenced by:  sucid  4966  nsuceq0  4967  trsuc  4971  sucssel  4979  ordsuc  6648  onpsssuc  6653  nlimsucg  6676  tfrlem11  7075  tfrlem13  7077  tz7.44-2  7091  omeulem1  7249  oeordi  7254  oeeulem  7268  php4  7723  wofib  7988  suc11reg  8053  cantnfle  8107  cantnflt2  8109  cantnfp1lem3  8116  cantnflem1  8125  cantnfleOLD  8137  cantnflt2OLD  8139  cantnfp1lem3OLD  8142  cantnflem1OLD  8148  dfac12lem1  8540  dfac12lem2  8541  ttukeylem3  8908  ttukeylem7  8912  r1wunlim  9132  ontgval  30101
 Copyright terms: Public domain W3C validator