Theorem peano2nn 11842

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 8170	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2		fvelrnb 6773	. . . 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 7246	. . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5		eqid 2737	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6		oveq1 7220	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7		oveq1 7220	. . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
8	5, 6, 7	frsucmpt2 8176	. . . . . . 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 7668	. . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11		fnfvelrn 6901	. . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
12	1, 10, 11	sylancr 590	. . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13		df-nn 11831	. . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14		df-ima 5564	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
15	13, 14	eqtri 2765	. . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
16	12, 15	eleqtrrdi 2849	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
17	9, 16	eqeltrrd 2839	. . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18		oveq1 7220	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
19	18	eleq1d 2822	. . . . 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 3199	. . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
22	3, 21	sylbi 220	. 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
23	22, 15	eleq2s 2856	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110  ∃wrex 3062  Vcvv 3408   ↦ cmpt 5135  ran crn 5552   ↾ cres 5553   “ cima 5554  suc csuc 6215   Fn wfn 6375  ‘cfv 6380  (class class class)co 7213  ωcom 7644  reccrdg 8145  1c1 10730   + caddc 10732  ℕcn 11830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-nn 11831

This theorem is referenced by:  dfnn2  11843  dfnn3  11844  peano2nnd  11847  nnind  11848  nnaddcl  11853  2nn  11903  3nn  11909  4nn  11913  5nn  11916  6nn  11919  7nn  11922  8nn  11925  9nn  11928  nnunb  12086  nneo  12261  10nn  12309  fzonn0p1p1  13321  ser1const  13632  expp1  13642  facp1  13844  relexpsucnnl  14593  isercolllem1  15228  isercoll2  15232  climcndslem2  15414  climcnds  15415  harmonic  15423  trireciplem  15426  trirecip  15427  rpnnen2lem9  15783  sqrt2irr  15810  nno  15943  nnoddm1d2  15947  rplpwr  16119  prmind2  16242  eulerthlem2  16335  pcmpt  16445  pockthi  16460  prmreclem6  16474  dec5nprm  16619  mulgnnp1  18500  chfacfisf  21751  chfacfisfcpmat  21752  cayhamlem1  21763  1stcfb  22342  bcthlem3  24223  bcthlem4  24224  ovolunlem1a  24393  ovolicc2lem4  24417  voliunlem1  24447  volsup  24453  volsup2  24502  itg1climres  24612  mbfi1fseqlem5  24617  itg2monolem1  24648  itg2i1fseqle  24652  itg2i1fseq  24653  itg2i1fseq2  24654  itg2addlem  24656  itg2gt0  24658  itg2cnlem1  24659  aaliou3lem7  25242  emcllem1  25878  emcllem2  25879  emcllem3  25880  emcllem5  25882  emcllem6  25883  emcllem7  25884  zetacvg  25897  lgam1  25946  bclbnd  26161  bposlem5  26169  2sqlem10  26309  dchrisumlem2  26371  logdivbnd  26437  pntrsumo1  26446  pntrsumbnd  26447  wwlksext2clwwlk  28140  numclwwlk2lem1  28459  numclwlk2lem2f  28460  opsqrlem5  30225  opsqrlem6  30226  nnindf  30853  psgnfzto1st  31091  esumpmono  31759  fibp1  32080  rrvsum  32133  subfacp1lem6  32860  subfaclim  32863  bcprod  33422  bccolsum  33423  iprodgam  33426  faclimlem1  33427  faclimlem2  33428  faclim2  33432  nn0prpwlem  34248  mblfinlem2  35552  volsupnfl  35559  seqpo  35642  incsequz  35643  incsequz2  35644  geomcau  35654  heiborlem6  35711  bfplem1  35717  fsuppind  39989  jm2.27dlem4  40537  nnsplit  42570  sumnnodd  42846  stoweidlem20  43236  wallispilem4  43284  wallispi2lem1  43287  wallispi2lem2  43288  stirlinglem4  43293  stirlinglem8  43297  stirlinglem11  43300  stirlinglem12  43301  stirlinglem13  43302  vonioolem2  43894  vonicclem2  43897  deccarry  44476  iccpartres  44543  iccelpart  44558  odz2prm2pw  44688  fmtnoprmfac1  44690  fmtnoprmfac2  44692  lighneallem4  44735