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

Theorem sucidg 4961
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 4950 . 2
42, 3mpbiri 233 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  =wceq 1395  e.wcel 1818  succsuc 4885
This theorem is referenced by:  sucid  4962  nsuceq0  4963  trsuc  4967  sucssel  4975  ordsuc  6649  onpsssuc  6654  nlimsucg  6677  tfrlem11  7076  tfrlem13  7078  tz7.44-2  7092  omeulem1  7250  oeordi  7255  oeeulem  7269  php4  7724  wofib  7991  suc11reg  8057  cantnfle  8111  cantnflt2  8113  cantnfp1lem3  8120  cantnflem1  8129  cantnfleOLD  8141  cantnflt2OLD  8143  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  dfac12lem1  8544  dfac12lem2  8545  ttukeylem3  8912  ttukeylem7  8916  r1wunlim  9136  ontgval  29896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-suc 4889
  Copyright terms: Public domain W3C validator