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

Theorem peano2nn 10879
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 7394 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2 fvelrnb 6138 . . . 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 6555 . . . . . . 7 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5 eqid 2609 . . . . . . . 8 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6 oveq1 6534 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7 oveq1 6534 . . . . . . . 8 (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
85, 6, 7frsucmpt2 7399 . . . . . . 7 ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
94, 8mpan2 702 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10 peano2 6955 . . . . . . . 8 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11 fnfvelrn 6249 . . . . . . . 8 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
121, 10, 11sylancr 693 . . . . . . 7 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13 df-nn 10868 . . . . . . . 8 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14 df-ima 5041 . . . . . . . 8 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1513, 14eqtri 2631 . . . . . . 7 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
1612, 15syl6eleqr 2698 . . . . . 6 (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
179, 16eqeltrrd 2688 . . . . 5 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18 oveq1 6534 . . . . . 6 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
1918eleq1d 2671 . . . . 5 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
2017, 19syl5ibcom 233 . . . 4 (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
2120rexlimiv 3008 . . 3 (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
223, 21sylbi 205 . 2 (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
2322, 15eleq2s 2705 1 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  wrex 2896  Vcvv 3172  cmpt 4637  ran crn 5029  cres 5030  cima 5031  suc csuc 5628   Fn wfn 5785  cfv 5790  (class class class)co 6527  ωcom 6934  reccrdg 7369  1c1 9793   + caddc 9795  cn 10867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10868
This theorem is referenced by:  dfnn2  10880  dfnn3  10881  peano2nnd  10884  nnind  10885  nnaddcl  10889  2nn  11032  3nn  11033  4nn  11034  5nn  11035  6nn  11036  7nn  11037  8nn  11038  9nn  11039  10nnOLD  11040  nnunb  11135  nneo  11293  10nn  11346  fzonn0p1p1  12368  ser1const  12674  expp1  12684  facp1  12882  relexpsucnnl  13566  isercolllem1  14189  isercoll2  14193  climcndslem2  14367  climcnds  14368  harmonic  14376  trireciplem  14379  trirecip  14380  rpnnen2lem9  14736  sqrt2irr  14763  nno  14882  nnoddm1d2  14886  rplpwr  15060  prmind2  15182  eulerthlem2  15271  pcmpt  15380  pockthi  15395  prmreclem6  15409  dec5nprm  15554  mulgnnp1  17318  chfacfisf  20420  chfacfisfcpmat  20421  cayhamlem1  20432  1stcfb  21000  bcthlem3  22848  bcthlem4  22849  ovolunlem1a  22988  ovolicc2lem4  23012  voliunlem1  23042  volsup  23048  volsup2  23096  itg1climres  23204  mbfi1fseqlem5  23209  itg2monolem1  23240  itg2i1fseqle  23244  itg2i1fseq  23245  itg2i1fseq2  23246  itg2addlem  23248  itg2gt0  23250  itg2cnlem1  23251  aaliou3lem7  23825  emcllem1  24439  emcllem2  24440  emcllem3  24441  emcllem5  24443  emcllem6  24444  emcllem7  24445  zetacvg  24458  lgam1  24507  bclbnd  24722  bposlem5  24730  2sqlem10  24870  dchrisumlem2  24896  logdivbnd  24962  pntrsumo1  24971  pntrsumbnd  24972  wwlkext2clwwlk  26097  numclwwlk2lem1  26395  numclwlk2lem2f  26396  opsqrlem5  28193  opsqrlem6  28194  nnindf  28758  psgnfzto1st  28992  esumpmono  29274  fibp1  29596  rrvsum  29649  subfacp1lem6  30227  subfaclim  30230  bcprod  30683  bccolsum  30684  iprodgam  30687  faclimlem1  30688  faclimlem2  30689  faclim2  30693  nn0prpwlem  31293  mblfinlem2  32413  volsupnfl  32420  seqpo  32509  incsequz  32510  incsequz2  32511  geomcau  32521  heiborlem6  32581  bfplem1  32587  jm2.27dlem4  36393  nnsplit  38312  sumnnodd  38494  stoweidlem20  38710  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem4  38767  stirlinglem8  38771  stirlinglem11  38774  stirlinglem12  38775  stirlinglem13  38776  vonioolem2  39369  vonicclem2  39372  deccarry  39739  iccpartres  39754  iccelpart  39769  odz2prm2pw  39811  fmtnoprmfac1  39813  fmtnoprmfac2  39815  lighneallem4  39863  wwlksext2clwwlk  41226  av-numclwwlk2lem1  41527  av-numclwlk2lem2f  41528
  Copyright terms: Public domain W3C validator