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

Theorem sucidg 4688
 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 2442 . . 3
21olci 382 . 2
3 elsucg 4677 . 2
42, 3mpbiri 226 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 359   wceq 1653   wcel 1727   csuc 4612 This theorem is referenced by:  sucid  4689  nsuceq0  4690  trsuc  4695  sucssel  4703  ordsuc  4823  onpsssuc  4828  nlimsucg  4851  tfrlem11  6678  tfrlem13  6680  tz7.44-2  6694  omeulem1  6854  oeordi  6859  oeeulem  6873  php4  7323  wofib  7543  suc11reg  7603  cantnfle  7655  cantnflt2  7657  cantnfp1lem3  7665  cantnflem1  7674  dfac12lem1  8054  dfac12lem2  8055  ttukeylem3  8422  ttukeylem7  8426  r1wunlim  8643  ontgval  26212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-sn 3844  df-suc 4616
 Copyright terms: Public domain W3C validator