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

Theorem peano2nn 11639
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 8061 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2 fvelrnb 6720 . . . 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 2821 . . . . . . . 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 8067 . . . . . . 7 ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
94, 8mpan2 687 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10 peano2 7590 . . . . . . . 8 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11 fnfvelrn 6841 . . . . . . . 8 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
121, 10, 11sylancr 587 . . . . . . 7 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13 df-nn 11628 . . . . . . . 8 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14 df-ima 5562 . . . . . . . 8 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1513, 14eqtri 2844 . . . . . . 7 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1612, 15eleqtrrdi 2924 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
179, 16eqeltrrd 2914 . . . . 5 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18 oveq1 7152 . . . . . 6 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
1918eleq1d 2897 . . . . 5 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
2017, 19syl5ibcom 246 . . . 4 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
2120rexlimiv 3280 . . 3 (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
223, 21sylbi 218 . 2 (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
2322, 15eleq2s 2931 1 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wrex 3139  Vcvv 3495  cmpt 5138  ran crn 5550  cres 5551  cima 5552  suc csuc 6187   Fn wfn 6344  cfv 6349  (class class class)co 7145  ωcom 7568  reccrdg 8036  1c1 10527   + caddc 10529  cn 11627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628
This theorem is referenced by:  dfnn2  11640  dfnn3  11641  peano2nnd  11644  nnind  11645  nnaddcl  11649  2nn  11699  3nn  11705  4nn  11709  5nn  11712  6nn  11715  7nn  11718  8nn  11721  9nn  11724  nnunb  11882  nneo  12055  10nn  12103  fzonn0p1p1  13106  ser1const  13416  expp1  13426  facp1  13628  relexpsucnnl  14381  isercolllem1  15011  isercoll2  15015  climcndslem2  15195  climcnds  15196  harmonic  15204  trireciplem  15207  trirecip  15208  rpnnen2lem9  15565  sqrt2irr  15592  nno  15723  nnoddm1d2  15727  rplpwr  15897  prmind2  16019  eulerthlem2  16109  pcmpt  16218  pockthi  16233  prmreclem6  16247  dec5nprm  16392  mulgnnp1  18176  chfacfisf  21392  chfacfisfcpmat  21393  cayhamlem1  21404  1stcfb  21983  bcthlem3  23858  bcthlem4  23859  ovolunlem1a  24026  ovolicc2lem4  24050  voliunlem1  24080  volsup  24086  volsup2  24135  itg1climres  24244  mbfi1fseqlem5  24249  itg2monolem1  24280  itg2i1fseqle  24284  itg2i1fseq  24285  itg2i1fseq2  24286  itg2addlem  24288  itg2gt0  24290  itg2cnlem1  24291  aaliou3lem7  24867  emcllem1  25501  emcllem2  25502  emcllem3  25503  emcllem5  25505  emcllem6  25506  emcllem7  25507  zetacvg  25520  lgam1  25569  bclbnd  25784  bposlem5  25792  2sqlem10  25932  dchrisumlem2  25994  logdivbnd  26060  pntrsumo1  26069  pntrsumbnd  26070  wwlksext2clwwlk  27764  numclwwlk2lem1  28083  numclwlk2lem2f  28084  opsqrlem5  29849  opsqrlem6  29850  nnindf  30462  psgnfzto1st  30675  esumpmono  31238  fibp1  31559  rrvsum  31612  subfacp1lem6  32330  subfaclim  32333  bcprod  32868  bccolsum  32869  iprodgam  32872  faclimlem1  32873  faclimlem2  32874  faclim2  32878  nn0prpwlem  33568  mblfinlem2  34812  volsupnfl  34819  seqpo  34905  incsequz  34906  incsequz2  34907  geomcau  34917  heiborlem6  34977  bfplem1  34983  jm2.27dlem4  39489  nnsplit  41506  sumnnodd  41791  stoweidlem20  42186  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem4  42243  stirlinglem8  42247  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  vonioolem2  42844  vonicclem2  42847  deccarry  43392  iccpartres  43425  iccelpart  43440  odz2prm2pw  43572  fmtnoprmfac1  43574  fmtnoprmfac2  43576  lighneallem4  43622
  Copyright terms: Public domain W3C validator