Theorem peano2nn 12387

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 8481	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2		fvelrnb 6976	. . . 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 7484	. . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5		eqid 2763	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6		oveq1 7458	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7		oveq1 7458	. . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
8	5, 6, 7	frsucmpt2 8486	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
9	4, 8	mpan2 704	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10		peano2 7935	. . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11		fnfvelrn 7112	. . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
12	1, 10, 11	sylancr 599	. . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13		df-nn 12376	. . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14		df-ima 5671	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
15	13, 14	eqtri 2786	. . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
16	12, 15	eleqtrrdi 2875	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
17	9, 16	eqeltrrd 2865	. . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18		oveq1 7458	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
19	18	eleq1d 2849	. . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
20	17, 19	syl5ibcom 248	. . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
21	20	rexlimiv 3160	. . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
22	3, 21	sylbi 220	. 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
23	22, 15	eleq2s 2882	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  Vcvv 3454   ↦ cmpt 5192  ran crn 5659   ↾ cres 5660   “ cima 5661  suc csuc 6390   Fn wfn 6561  ‘cfv 6566  (class class class)co 7451  ωcom 7911  reccrdg 8455  1c1 11240   + caddc 11242  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376

This theorem is used by:  dfnn2  12388  dfnn3  12389  peano2nnd  12392  nnind  12393  nnaddcl  12398  2nn  12456  3nn  12462  4nn  12466  5nn  12469  6nn  12472  7nn  12475  8nn  12478  9nn  12481  nnunb  12642  nneo  12823  10nn  12874  fzonn0p1p1  13919  ser1const  14241  expp1  14251  facp1  14463  relexpsucnnl  15226  isercolllem1  15876  isercoll2  15880  climcndslem2  16063  climcnds  16064  harmonic  16072  trireciplem  16075  trirecip  16076  rpnnen2lem9  16434  sqrt2irr  16461  nno  16596  nnoddm1d2  16600  rplpwr  16776  prmind2  16904  eulerthlem2  17003  pcmpt  17114  pockthi  17129  prmreclem6  17143  dec5nprm  17288  mulgnnp1  19342  chfacfisf  23227  chfacfisfcpmat  23228  cayhamlem1  23239  1stcfb  23818  bcthlem3  25702  bcthlem4  25703  ovolunlem1a  25872  ovolicc2lem4  25896  voliunlem1  25926  volsup  25932  volsup2  25981  itg1climres  26090  mbfi1fseqlem5  26095  itg2monolem1  26126  itg2i1fseqle  26130  itg2i1fseq  26131  itg2i1fseq2  26132  itg2addlem  26134  itg2gt0  26136  itg2cnlem1  26137  aaliou3lem7  26733  emcllem1  27380  emcllem2  27381  emcllem3  27382  emcllem5  27384  emcllem6  27385  emcllem7  27386  zetacvg  27399  lgam1  27448  bclbnd  27664  bposlem5  27672  2sqlem10  27812  dchrisumlem2  27874  logdivbnd  27940  pntrsumo1  27949  pntrsumbnd  27950  wwlksext2clwwlk  30705  numclwwlk2lem1  31034  numclwlk2lem2f  31035  opsqrlem5  32803  opsqrlem6  32804  nnindf  33507  psgnfzto1st  33765  esumpmono  34822  fibp1  35144  rrvsum  35197  subfacp1lem6  36158  subfaclim  36161  bcprod  36718  bccolsum  36719  iprodgam  36722  faclimlem1  36723  faclimlem2  36724  faclim2  36728  nn0prpwlem  37325  mblfinlem2  38844  volsupnfl  38851  seqpo  38947  incsequz  38948  incsequz2  38949  geomcau  38959  heiborlem6  39016  bfplem1  39022  fimgmcyc  43864  fsuppind  43884  jm2.27dlem4  44285  nnsplit  46643  sumnnodd  46915  stoweidlem20  47303  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem4  47360  stirlinglem8  47364  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  vonioolem2  47964  vonicclem2  47967  deccarry  48654  iccpartres  48773  iccelpart  48788  odz2prm2pw  48921  fmtnoprmfac1  48923  fmtnoprmfac2  48925  lighneallem4  48968