Theorem peano2nn 11985

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.

Step	Hyp	Ref	Expression
1		frfnom 8266	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2		fvelrnb 6830	. . . 4 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω → (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴))
3	1, 2	ax-mp 5	. . 3 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴)
4		ovex 7308	. . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5		eqid 2738	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6		oveq1 7282	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7		oveq1 7282	. . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
8	5, 6, 7	frsucmpt2 8271	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
9	4, 8	mpan2 688	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10		peano2 7737	. . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11		fnfvelrn 6958	. . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
12	1, 10, 11	sylancr 587	. . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13		df-nn 11974	. . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14		df-ima 5602	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
15	13, 14	eqtri 2766	. . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
16	12, 15	eleqtrrdi 2850	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
17	9, 16	eqeltrrd 2840	. . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18		oveq1 7282	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
19	18	eleq1d 2823	. . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
20	17, 19	syl5ibcom 244	. . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
21	20	rexlimiv 3209	. . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
22	3, 21	sylbi 216	. 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
23	22, 15	eleq2s 2857	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  ∃wrex 3065  Vcvv 3432   ↦ cmpt 5157  ran crn 5590   ↾ cres 5591   “ cima 5592  suc csuc 6268   Fn wfn 6428  ‘cfv 6433  (class class class)co 7275  ωcom 7712  reccrdg 8240  1c1 10872   + caddc 10874  ℕcn 11973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-nn 11974

This theorem is referenced by:  dfnn2  11986  dfnn3  11987  peano2nnd  11990  nnind  11991  nnaddcl  11996  2nn  12046  3nn  12052  4nn  12056  5nn  12059  6nn  12062  7nn  12065  8nn  12068  9nn  12071  nnunb  12229  nneo  12404  10nn  12453  fzonn0p1p1  13466  ser1const  13779  expp1  13789  facp1  13992  relexpsucnnl  14741  isercolllem1  15376  isercoll2  15380  climcndslem2  15562  climcnds  15563  harmonic  15571  trireciplem  15574  trirecip  15575  rpnnen2lem9  15931  sqrt2irr  15958  nno  16091  nnoddm1d2  16095  rplpwr  16267  prmind2  16390  eulerthlem2  16483  pcmpt  16593  pockthi  16608  prmreclem6  16622  dec5nprm  16767  mulgnnp1  18712  chfacfisf  22003  chfacfisfcpmat  22004  cayhamlem1  22015  1stcfb  22596  bcthlem3  24490  bcthlem4  24491  ovolunlem1a  24660  ovolicc2lem4  24684  voliunlem1  24714  volsup  24720  volsup2  24769  itg1climres  24879  mbfi1fseqlem5  24884  itg2monolem1  24915  itg2i1fseqle  24919  itg2i1fseq  24920  itg2i1fseq2  24921  itg2addlem  24923  itg2gt0  24925  itg2cnlem1  24926  aaliou3lem7  25509  emcllem1  26145  emcllem2  26146  emcllem3  26147  emcllem5  26149  emcllem6  26150  emcllem7  26151  zetacvg  26164  lgam1  26213  bclbnd  26428  bposlem5  26436  2sqlem10  26576  dchrisumlem2  26638  logdivbnd  26704  pntrsumo1  26713  pntrsumbnd  26714  wwlksext2clwwlk  28421  numclwwlk2lem1  28740  numclwlk2lem2f  28741  opsqrlem5  30506  opsqrlem6  30507  nnindf  31133  psgnfzto1st  31372  esumpmono  32047  fibp1  32368  rrvsum  32421  subfacp1lem6  33147  subfaclim  33150  bcprod  33704  bccolsum  33705  iprodgam  33708  faclimlem1  33709  faclimlem2  33710  faclim2  33714  nn0prpwlem  34511  mblfinlem2  35815  volsupnfl  35822  seqpo  35905  incsequz  35906  incsequz2  35907  geomcau  35917  heiborlem6  35974  bfplem1  35980  fsuppind  40279  jm2.27dlem4  40834  nnsplit  42897  sumnnodd  43171  stoweidlem20  43561  wallispilem4  43609  wallispi2lem1  43612  wallispi2lem2  43613  stirlinglem4  43618  stirlinglem8  43622  stirlinglem11  43625  stirlinglem12  43626  stirlinglem13  43627  vonioolem2  44219  vonicclem2  44222  deccarry  44803  iccpartres  44870  iccelpart  44885  odz2prm2pw  45015  fmtnoprmfac1  45017  fmtnoprmfac2  45019  lighneallem4  45062