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

Theorem peano2nn 11655
 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 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nn
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frfnom 8071 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2 fvelrnb 6711 . . . 4 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω → (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴))
31, 2ax-mp 5 . . 3 (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴)
4 ovex 7178 . . . . . . 7 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5 eqid 2798 . . . . . . . 8 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6 oveq1 7152 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7 oveq1 7152 . . . . . . . 8 (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
85, 6, 7frsucmpt2 8077 . . . . . . 7 ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
94, 8mpan2 690 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10 peano2 7595 . . . . . . . 8 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11 fnfvelrn 6835 . . . . . . . 8 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
121, 10, 11sylancr 590 . . . . . . 7 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13 df-nn 11644 . . . . . . . 8 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14 df-ima 5536 . . . . . . . 8 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1513, 14eqtri 2821 . . . . . . 7 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1612, 15eleqtrrdi 2901 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
179, 16eqeltrrd 2891 . . . . 5 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18 oveq1 7152 . . . . . 6 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
1918eleq1d 2874 . . . . 5 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
2017, 19syl5ibcom 248 . . . 4 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
2120rexlimiv 3240 . . 3 (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
223, 21sylbi 220 . 2 (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
2322, 15eleq2s 2908 1 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  Vcvv 3442   ↦ cmpt 5114  ran crn 5524   ↾ cres 5525   “ cima 5526  suc csuc 6168   Fn wfn 6327  ‘cfv 6332  (class class class)co 7145  ωcom 7573  reccrdg 8046  1c1 10545   + caddc 10547  ℕcn 11643 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-ov 7148  df-om 7574  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-nn 11644 This theorem is referenced by:  dfnn2  11656  dfnn3  11657  peano2nnd  11660  nnind  11661  nnaddcl  11666  2nn  11716  3nn  11722  4nn  11726  5nn  11729  6nn  11732  7nn  11735  8nn  11738  9nn  11741  nnunb  11899  nneo  12074  10nn  12122  fzonn0p1p1  13131  ser1const  13442  expp1  13452  facp1  13654  relexpsucnnl  14401  isercolllem1  15033  isercoll2  15037  climcndslem2  15217  climcnds  15218  harmonic  15226  trireciplem  15229  trirecip  15230  rpnnen2lem9  15587  sqrt2irr  15614  nno  15743  nnoddm1d2  15747  rplpwr  15917  prmind2  16039  eulerthlem2  16129  pcmpt  16238  pockthi  16253  prmreclem6  16267  dec5nprm  16412  mulgnnp1  18249  chfacfisf  21500  chfacfisfcpmat  21501  cayhamlem1  21512  1stcfb  22091  bcthlem3  23971  bcthlem4  23972  ovolunlem1a  24141  ovolicc2lem4  24165  voliunlem1  24195  volsup  24201  volsup2  24250  itg1climres  24359  mbfi1fseqlem5  24364  itg2monolem1  24395  itg2i1fseqle  24399  itg2i1fseq  24400  itg2i1fseq2  24401  itg2addlem  24403  itg2gt0  24405  itg2cnlem1  24406  aaliou3lem7  24989  emcllem1  25625  emcllem2  25626  emcllem3  25627  emcllem5  25629  emcllem6  25630  emcllem7  25631  zetacvg  25644  lgam1  25693  bclbnd  25908  bposlem5  25916  2sqlem10  26056  dchrisumlem2  26118  logdivbnd  26184  pntrsumo1  26193  pntrsumbnd  26194  wwlksext2clwwlk  27886  numclwwlk2lem1  28205  numclwlk2lem2f  28206  opsqrlem5  29971  opsqrlem6  29972  nnindf  30605  psgnfzto1st  30846  esumpmono  31514  fibp1  31835  rrvsum  31888  subfacp1lem6  32611  subfaclim  32614  bcprod  33153  bccolsum  33154  iprodgam  33157  faclimlem1  33158  faclimlem2  33159  faclim2  33163  nn0prpwlem  33930  mblfinlem2  35246  volsupnfl  35253  seqpo  35336  incsequz  35337  incsequz2  35338  geomcau  35348  heiborlem6  35405  bfplem1  35411  fsuppind  39624  jm2.27dlem4  40124  nnsplit  42158  sumnnodd  42440  stoweidlem20  42830  wallispilem4  42878  wallispi2lem1  42881  wallispi2lem2  42882  stirlinglem4  42887  stirlinglem8  42891  stirlinglem11  42894  stirlinglem12  42895  stirlinglem13  42896  vonioolem2  43488  vonicclem2  43491  deccarry  44036  iccpartres  44103  iccelpart  44118  odz2prm2pw  44248  fmtnoprmfac1  44250  fmtnoprmfac2  44252  lighneallem4  44296
 Copyright terms: Public domain W3C validator