Theorem peano2nn 12257

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 8454	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2		fvelrnb 6944	. . . 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 7443	. . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5		eqid 2736	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6		oveq1 7417	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7		oveq1 7417	. . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
8	5, 6, 7	frsucmpt2 8459	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
9	4, 8	mpan2 691	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10		peano2 7891	. . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11		fnfvelrn 7075	. . . . . . . 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 12246	. . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14		df-ima 5672	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
15	13, 14	eqtri 2759	. . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
16	12, 15	eleqtrrdi 2846	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
17	9, 16	eqeltrrd 2836	. . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18		oveq1 7417	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
19	18	eleq1d 2820	. . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
20	17, 19	syl5ibcom 245	. . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
21	20	rexlimiv 3135	. . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
22	3, 21	sylbi 217	. 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
23	22, 15	eleq2s 2853	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3061  Vcvv 3464   ↦ cmpt 5206  ran crn 5660   ↾ cres 5661   “ cima 5662  suc csuc 6359   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  ωcom 7866  reccrdg 8428  1c1 11135   + caddc 11137  ℕcn 12245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-nn 12246

This theorem is referenced by:  dfnn2  12258  dfnn3  12259  peano2nnd  12262  nnind  12263  nnaddcl  12268  2nn  12318  3nn  12324  4nn  12328  5nn  12331  6nn  12334  7nn  12337  8nn  12340  9nn  12343  nnunb  12502  nneo  12682  10nn  12729  fzonn0p1p1  13765  ser1const  14081  expp1  14091  facp1  14301  relexpsucnnl  15054  isercolllem1  15686  isercoll2  15690  climcndslem2  15871  climcnds  15872  harmonic  15880  trireciplem  15883  trirecip  15884  rpnnen2lem9  16245  sqrt2irr  16272  nno  16406  nnoddm1d2  16410  rplpwr  16582  prmind2  16709  eulerthlem2  16806  pcmpt  16917  pockthi  16932  prmreclem6  16946  dec5nprm  17091  mulgnnp1  19070  chfacfisf  22797  chfacfisfcpmat  22798  cayhamlem1  22809  1stcfb  23388  bcthlem3  25283  bcthlem4  25284  ovolunlem1a  25454  ovolicc2lem4  25478  voliunlem1  25508  volsup  25514  volsup2  25563  itg1climres  25672  mbfi1fseqlem5  25677  itg2monolem1  25708  itg2i1fseqle  25712  itg2i1fseq  25713  itg2i1fseq2  25714  itg2addlem  25716  itg2gt0  25718  itg2cnlem1  25719  aaliou3lem7  26314  emcllem1  26963  emcllem2  26964  emcllem3  26965  emcllem5  26967  emcllem6  26968  emcllem7  26969  zetacvg  26982  lgam1  27031  bclbnd  27248  bposlem5  27256  2sqlem10  27396  dchrisumlem2  27458  logdivbnd  27524  pntrsumo1  27533  pntrsumbnd  27534  wwlksext2clwwlk  30043  numclwwlk2lem1  30362  numclwlk2lem2f  30363  opsqrlem5  32130  opsqrlem6  32131  nnindf  32803  psgnfzto1st  33121  esumpmono  34115  fibp1  34438  rrvsum  34491  subfacp1lem6  35212  subfaclim  35215  bcprod  35760  bccolsum  35761  iprodgam  35764  faclimlem1  35765  faclimlem2  35766  faclim2  35770  nn0prpwlem  36345  mblfinlem2  37687  volsupnfl  37694  seqpo  37776  incsequz  37777  incsequz2  37778  geomcau  37788  heiborlem6  37845  bfplem1  37851  fimgmcyc  42524  fsuppind  42580  jm2.27dlem4  43003  nnsplit  45352  sumnnodd  45626  stoweidlem20  46016  wallispilem4  46064  wallispi2lem1  46067  wallispi2lem2  46068  stirlinglem4  46073  stirlinglem8  46077  stirlinglem11  46080  stirlinglem12  46081  stirlinglem13  46082  vonioolem2  46677  vonicclem2  46680  deccarry  47307  iccpartres  47399  iccelpart  47414  odz2prm2pw  47544  fmtnoprmfac1  47546  fmtnoprmfac2  47548  lighneallem4  47591