Theorem peano2nn 12216

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 8400	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
2		fvelrnb 6922	. . . 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 7424	. . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V
5		eqid 2761	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
6		oveq1 7398	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1))
7		oveq1 7398	. . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
8	5, 6, 7	frsucmpt2 8405	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
9	4, 8	mpan2 701	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1))
10		peano2 7865	. . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
11		fnfvelrn 7056	. . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
12	1, 10, 11	sylancr 596	. . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
13		df-nn 12205	. . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
14		df-ima 5656	. . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
15	13, 14	eqtri 2784	. . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
16	12, 15	eleqtrrdi 2872	. . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ)
17	9, 16	eqeltrrd 2862	. . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ)
18		oveq1 7398	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1))
19	18	eleq1d 2846	. . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ))
20	17, 19	syl5ibcom 247	. . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ))
21	20	rexlimiv 3155	. . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)
22	3, 21	sylbi 219	. 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ)
23	22, 15	eleq2s 2879	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∃wrex 3085  Vcvv 3453   ↦ cmpt 5178  ran crn 5644   ↾ cres 5645   “ cima 5646  suc csuc 6343   Fn wfn 6511  ‘cfv 6516  (class class class)co 7391  ωcom 7841  reccrdg 8374  1c1 11068   + caddc 11070  ℕcn 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205

This theorem is referenced by:  dfnn2  12217  dfnn3  12218  peano2nnd  12221  nnind  12222  nnaddcl  12227  2nn  12285  3nn  12291  4nn  12295  5nn  12298  6nn  12301  7nn  12304  8nn  12307  9nn  12310  nnunb  12471  nneo  12651  10nn  12702  fzonn0p1p1  13744  ser1const  14065  expp1  14075  facp1  14285  relexpsucnnl  15037  isercolllem1  15683  isercoll2  15687  climcndslem2  15871  climcnds  15872  harmonic  15880  trireciplem  15883  trirecip  15884  rpnnen2lem9  16245  sqrt2irr  16272  nno  16407  nnoddm1d2  16411  rplpwr  16583  prmind2  16710  eulerthlem2  16808  pcmpt  16919  pockthi  16934  prmreclem6  16948  dec5nprm  17093  mulgnnp1  19115  chfacfisf  22902  chfacfisfcpmat  22903  cayhamlem1  22914  1stcfb  23493  bcthlem3  25376  bcthlem4  25377  ovolunlem1a  25546  ovolicc2lem4  25570  voliunlem1  25600  volsup  25606  volsup2  25655  itg1climres  25764  mbfi1fseqlem5  25769  itg2monolem1  25800  itg2i1fseqle  25804  itg2i1fseq  25805  itg2i1fseq2  25806  itg2addlem  25808  itg2gt0  25810  itg2cnlem1  25811  aaliou3lem7  26401  emcllem1  27048  emcllem2  27049  emcllem3  27050  emcllem5  27052  emcllem6  27053  emcllem7  27054  zetacvg  27067  lgam1  27116  bclbnd  27332  bposlem5  27340  2sqlem10  27480  dchrisumlem2  27542  logdivbnd  27608  pntrsumo1  27617  pntrsumbnd  27618  wwlksext2clwwlk  30216  numclwwlk2lem1  30535  numclwlk2lem2f  30536  opsqrlem5  32304  opsqrlem6  32305  nnindf  32983  psgnfzto1st  33246  esumpmono  34337  fibp1  34659  rrvsum  34712  subfacp1lem6  35496  subfaclim  35499  bcprod  36049  bccolsum  36050  iprodgam  36053  faclimlem1  36054  faclimlem2  36055  faclim2  36059  nn0prpwlem  36643  mblfinlem2  38118  volsupnfl  38125  seqpo  38207  incsequz  38208  incsequz2  38209  geomcau  38219  heiborlem6  38276  bfplem1  38282  fimgmcyc  43113  fsuppind  43133  jm2.27dlem4  43550  nnsplit  45895  sumnnodd  46167  stoweidlem20  46555  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  stirlinglem4  46612  stirlinglem8  46616  stirlinglem11  46619  stirlinglem12  46620  stirlinglem13  46621  vonioolem2  47216  vonicclem2  47219  deccarry  47866  iccpartres  47985  iccelpart  48000  odz2prm2pw  48133  fmtnoprmfac1  48135  fmtnoprmfac2  48137  lighneallem4  48180