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

Theorem peano2nn 10573
 Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
peano2nn

Proof of Theorem peano2nn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frfnom 7119 . . . 4
2 fvelrnb 5920 . . . 4
31, 2ax-mp 5 . . 3
4 ovex 6324 . . . . . . 7
5 eqid 2457 . . . . . . . 8
6 oveq1 6303 . . . . . . . 8
7 oveq1 6303 . . . . . . . 8
85, 6, 7frsucmpt2 7124 . . . . . . 7
94, 8mpan2 671 . . . . . 6
10 peano2 6720 . . . . . . . 8
11 fnfvelrn 6028 . . . . . . . 8
121, 10, 11sylancr 663 . . . . . . 7
13 df-nn 10562 . . . . . . . 8
14 df-ima 5017 . . . . . . . 8
1513, 14eqtri 2486 . . . . . . 7
1612, 15syl6eleqr 2556 . . . . . 6
179, 16eqeltrrd 2546 . . . . 5
18 oveq1 6303 . . . . . 6
1918eleq1d 2526 . . . . 5
2017, 19syl5ibcom 220 . . . 4
2120rexlimiv 2943 . . 3
223, 21sylbi 195 . 2
2322, 15eleq2s 2565 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  E.wrex 2808   cvv 3109  e.cmpt 4510  succsuc 4885  rancrn 5005  |cres 5006  "cima 5007  Fnwfn 5588  cfv 5593  (class class class)co 6296   com 6700  reccrdg 7094  1c1 9514   caddc 9516   cn 10561 This theorem is referenced by:  dfnn2  10574  dfnn3  10575  peano2nnd  10578  nnind  10579  nnaddcl  10583  2nn  10718  3nn  10719  4nn  10720  5nn  10721  6nn  10722  7nn  10723  8nn  10724  9nn  10725  10nn  10726  nnunb  10816  nneo  10971  fzonn0p1p1  11894  ser1const  12163  expp1  12173  facp1  12358  isercolllem1  13487  isercoll2  13491  climcndslem2  13662  climcnds  13663  harmonic  13670  trireciplem  13673  trirecip  13674  rpnnen2lem9  13956  sqrt2irr  13982  rplpwr  14194  prmind2  14228  eulerthlem2  14312  pcmpt  14411  pockthi  14425  prmreclem6  14439  dec5nprm  14552  mulgnnp1  16150  chfacfisf  19355  chfacfisfcpmat  19356  cayhamlem1  19367  1stcfb  19946  bcthlem3  21765  bcthlem4  21766  ovolunlem1a  21907  ovolicc2lem4  21931  voliunlem1  21960  volsup  21966  volsup2  22014  itg1climres  22121  mbfi1fseqlem5  22126  itg2monolem1  22157  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  aaliou3lem7  22745  emcllem1  23325  emcllem2  23326  emcllem3  23327  emcllem5  23329  emcllem6  23330  emcllem7  23331  bclbnd  23555  bposlem5  23563  2sqlem10  23649  dchrisumlem2  23675  logdivbnd  23741  pntrsumo1  23750  pntrsumbnd  23751  wwlkext2clwwlk  24803  numclwwlk2lem1  25102  numclwlk2lem2f  25103  gxnn0suc  25266  opsqrlem5  27063  opsqrlem6  27064  nnindf  27610  esumpmono  28085  fibp1  28340  rrvsum  28393  zetacvg  28557  lgam1  28606  subfacp1lem6  28629  subfaclim  28632  iprodgam  29125  faclimlem1  29168  faclimlem2  29169  faclim2  29173  mblfinlem2  30052  volsupnfl  30059  nn0prpwlem  30140  seqpo  30240  incsequz  30241  incsequz2  30242  geomcau  30252  heiborlem6  30312  bfplem1  30318  jm2.27dlem4  30954  sumnnodd  31636  stoweidlem20  31802  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  stirlinglem4  31859  stirlinglem8  31863  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868 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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562
 Copyright terms: Public domain W3C validator