Theorem 1nn 12339

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
1nn	⊢ 1 ∈ ℕ

Proof of Theorem 1nn

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1ex 11296	. . . 4 ⊢ 1 ∈ V
2		fr0g 8437	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8436	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7898	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7078	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 705	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2858	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12329	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5664	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2784	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2860	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279   ↦ cmpt 5186  ran crn 5652   ↾ cres 5653   “ cima 5654   Fn wfn 6532  ‘cfv 6537  (class class class)co 7418  ωcom 7875  reccrdg 8410  1c1 11194   + caddc 11196  ℕcn 12328

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-1cn 11251

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-nn 12329

This theorem is used by:  dfnn2  12341  dfnn3  12342  nnind  12346  nn1suc  12350  nnmulcom  12389  2nn  12409  nnunb  12595  1nn0  12615  nn0p1nn  12638  elz2  12704  1z  12719  neg1z  12725  0nn0m1nnn0  12746  nneo  12776  9p1e10  12809  11nn  12832  elnn1uz2  13045  zq  13074  rpnnen1lem4  13101  rpnnen1lem5  13102  1elfzo1  13842  ser1const  14194  exp1  14203  nnexpcl  14210  expnbnd  14369  fac1  14414  faccl  14420  faclbnd3  14429  faclbnd4lem1  14430  faclbnd4lem2  14431  faclbnd4lem3  14432  faclbnd4lem4  14433  lsw0  14703  ccat2s1p1  14770  cats1un  14863  revs1  14907  cats1fvn  15002  relexpsucnnl  15176  relexpaddg  15199  isercolllem2  15826  isercolllem3  15827  isercoll  15828  sumsnf  15902  climcndslem1  16011  climcndslem2  16012  fprodnncl  16115  prodsn  16122  prodsnf  16124  nnrisefaccl  16179  eftlub  16270  eirrlem  16365  rpnnen2lem5  16379  rpnnen2lem8  16382  rpnnen2lem12  16386  dvdsle  16473  ndvdsp1  16574  5ndvds6  16577  gcd1  16694  bezoutr1  16737  1nprm  16847  1idssfct  16848  isprm2lem  16849  qden1elz  16926  phi1  16943  phiprm  16947  pcpre1  17013  pczpre  17018  pcmptcl  17062  pcmpt  17063  infpnlem2  17082  prmreclem1  17087  prmreclem6  17092  mul4sq  17125  vdwmc2  17150  vdwlem8  17159  vdwlem13  17164  vdwnnlem3  17168  prmocl  17205  prmop1  17209  fvprmselelfz  17215  fvprmselgcd1  17216  prmolefac  17217  prmodvdslcmf  17218  prmgapprmo  17233  5prm  17279  7prm  17281  10nprm  17284  11prm  17286  13prm  17287  17prm  17288  19prm  17289  37prm  17292  43prm  17293  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem4  17305  1259lem5  17306  1259prm  17307  2503lem3  17310  2503prm  17311  4001lem1  17312  4001lem2  17313  4001lem3  17314  4001lem4  17315  4001prm  17316  baseid  17383  basendx  17389  basendxnn  17390  rngstr  17462  lmodstr  17489  topgrpstr  17525  otpsstr  17540  ocndx  17545  ocid  17546  basendxnocndx  17547  plendxnocndx  17548  basendxltdsndx  17552  dsndxnplusgndx  17554  dsndxnmulrndx  17555  slotsdnscsi  17556  dsndxntsetndx  17557  slotsdifdsndx  17558  basendxltunifndx  17562  unifndxntsetndx  17564  slotsdifunifndx  17565  slotsbhcdif  17579  slotsdifocndx  17581  catstr  18128  ipostr  18696  mulgfval  19272  mulg1  19284  mulg2  19286  od1  19766  0subgALT  19775  gex1  19798  efgsval2  19940  efgsp1  19944  torsubg  20061  pgpfaclem1  20290  pmatcollpw3fi1lem2  23098  hauspwdom  23813  imasdsf1olem  24685  cphipval  25557  bcthlem4  25641  bcth3  25645  ovolmge0  25791  ovollb2  25803  ovolctb  25804  ovolunlem1a  25810  ovolunlem1  25811  ovoliunlem1  25816  ovoliun  25819  ovoliun2  25820  ovolicc1  25830  voliunlem1  25864  volsup  25870  ioombl1lem2  25873  ioombl1lem4  25875  uniioombllem1  25895  uniioombllem2  25897  uniioombllem6  25902  itg1climres  26028  itg2seq  26056  itg2monolem1  26064  itg2monolem2  26065  itg2monolem3  26066  itg2mono  26067  itg2i1fseq2  26070  itg2cnlem1  26075  aalioulem5  26656  aaliou2b  26661  aaliou3lem4  26666  aaliou3lem7  26669  log2ub  27270  emcllem6  27321  emcllem7  27322  lgam1  27384  gam1  27385  ftalem7  27399  efnnfsumcl  27423  vmaprm  27437  efvmacl  27440  efchtdvds  27479  vma1  27486  prmorcht  27498  sqff1o  27502  pclogsum  27535  perfectlem1  27549  perfectlem2  27550  bpos1  27603  bposlem5  27608  lgsdir  27652  lgs1  27661  lgsquad2lem2  27705  addsqn2reu  27761  addsqrexnreu  27762  dchrmusumlema  27813  dchrisum0lema  27834  slotsinbpsd  28896  slotslnbpsd  28897  trkgstr  28899  angmgmlem  29388  angmgmbas  29391  eengstr  29551  basendxltedgfndx  29565  usgrexmplef  29833  lfgrn1cycl  30387  clwwlkn1  30625  ipval2  31302  opsqrlem2  32736  ssnnssfz  33372  znumd  33397  zdend  33398  nnindf  33404  nn0min  33405  isarchi3  33741  eufndx  33847  eufid  33848  constrext2chnlem  34375  iconstr  34391  rge0scvg  34574  qqh0  34609  qqh1  34610  esumfzf  34694  esumfsup  34695  esumpcvgval  34703  voliune  34855  eulerpartgbij  34997  eulerpartlemgs2  35005  fib2  35027  rrvsum  35079  ballotlem4  35124  ballotlemi1  35128  ballotlemii  35129  ballotlemic  35132  ballotlem1c  35133  hgt750lem  35273  hgt750leme  35280  faclimlem1  36487  nn0prpwlem  37090  nn0prpw  37091  poimirlem32  38550  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  incsequz  38662  bfplem1  38736  rrncmslem  38746  60gcd7e1  43035  12lcm5e60  43038  60lcm7e420  43040  lcm1un  43043  lcmineqlem10  43068  3lexlogpow5ineq1  43084  3lexlogpow5ineq2  43085  aks4d1p1p7  43104  aks6d1c1p8  43145  sticksstones9  43184  sticksstones11  43186  aks6d1c7lem1  43210  3cubes  43680  jm2.23  43982  rmydioph  44000  rmxdioph  44002  expdiophlem2  44008  expdioph  44009  relexp2  44662  iunrelexpmin1  44693  iunrelexpmin2  44697  dftrcl3  44705  fvtrcllb1d  44707  cotrcltrcl  44710  corcltrcl  44724  cotrclrcl  44727  prmunb2  45280  sumsnd  46012  nnn0  46358  xrralrecnnge  46370  iooiinicc  46523  iooiinioc  46537  mccl  46579  sumnnodd  46611  wallispilem4  47047  wallispi2lem1  47050  wallispi2lem2  47051  stirlinglem8  47060  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  fourierdlem31  47117  nnfoctbdjlem  47434  hoicvrrex  47535  hoidmvlelem3  47576  ovnhoilem1  47580  ovnhoilem2  47581  ovnlecvr2  47589  ovnsubadd2lem  47624  iinhoiicclem  47652  vonicclem2  47663  numtowerdt  47885  1elfzo1ceilhalf1  48380  iccpartlt  48475  257prm  48615  fmtnoprmfac2lem1  48620  fmtno4prmfac193  48627  fmtno4nprmfac193  48628  fmtno5nprm  48637  3ndvds4  48649  139prmALT  48650  31prm  48651  127prm  48653  3exp4mod41  48670  41prothprmlem2  48672  perfectALTVlem1  48788  perfectALTVlem2  48789  2exp340mod341  48800  341fppr2  48801  4fppr1  48802  nnsum3primesprm  48857  bgoldbtbndlem1  48872  tgblthelfgott  48882  nnsgrpmgm  49242  nnsgrpnmnd  49244  blennn0elnn  49658  blen1  49665  ackval42  49777  1elfz13  50912  veronesevrowd  50948  veronesematrowd  50950  veroquadgsumlem  50952  veroquadmodzerod  50953  veroquadnolindfd  50954