Theorem 1nn 12268

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 11227	. . . 4 ⊢ 1 ∈ V
2		fr0g 8425	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8424	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7885	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7073	. . . 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 2857	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12258	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5668	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2783	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2859	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ∅c0 4279   ↦ cmpt 5186  ran crn 5656   ↾ cres 5657   “ cima 5658   Fn wfn 6528  ‘cfv 6533  (class class class)co 7413  ωcom 7862  reccrdg 8398  1c1 11125   + caddc 11127  ℕcn 12257

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12258

This theorem is used by:  dfnn2  12270  dfnn3  12271  nnind  12275  nn1suc  12279  nnmulcom  12318  2nn  12338  nnunb  12524  1nn0  12544  nn0p1nn  12567  elz2  12633  1z  12648  neg1z  12654  0nn0m1nnn0  12675  nneo  12705  9p1e10  12738  11nn  12761  elnn1uz2  12974  zq  13003  rpnnen1lem4  13030  rpnnen1lem5  13031  1elfzo1  13770  ser1const  14122  exp1  14131  nnexpcl  14138  expnbnd  14296  fac1  14341  faccl  14347  faclbnd3  14356  faclbnd4lem1  14357  faclbnd4lem2  14358  faclbnd4lem3  14359  faclbnd4lem4  14360  lsw0  14630  ccat2s1p1  14697  cats1un  14790  revs1  14834  cats1fvn  14929  relexpsucnnl  15103  relexpaddg  15126  isercolllem2  15753  isercolllem3  15754  isercoll  15755  sumsnf  15829  climcndslem1  15938  climcndslem2  15939  fprodnncl  16042  prodsn  16049  prodsnf  16051  nnrisefaccl  16106  eftlub  16197  eirrlem  16292  rpnnen2lem5  16306  rpnnen2lem8  16309  rpnnen2lem12  16313  dvdsle  16400  ndvdsp1  16501  5ndvds6  16504  gcd1  16618  bezoutr1  16659  1nprm  16769  1idssfct  16770  isprm2lem  16771  qden1elz  16848  phi1  16864  phiprm  16868  pcpre1  16934  pczpre  16939  pcmptcl  16983  pcmpt  16984  infpnlem2  17003  prmreclem1  17008  prmreclem6  17013  mul4sq  17046  vdwmc2  17071  vdwlem8  17080  vdwlem13  17085  vdwnnlem3  17089  prmocl  17126  prmop1  17130  fvprmselelfz  17136  fvprmselgcd1  17137  prmolefac  17138  prmodvdslcmf  17139  prmgapprmo  17154  5prm  17200  7prm  17202  10nprm  17205  11prm  17207  13prm  17208  17prm  17209  19prm  17210  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  baseid  17304  basendx  17310  basendxnn  17311  rngstr  17383  lmodstr  17410  topgrpstr  17446  otpsstr  17461  ocndx  17466  ocid  17467  basendxnocndx  17468  plendxnocndx  17469  basendxltdsndx  17473  dsndxnplusgndx  17475  dsndxnmulrndx  17476  slotsdnscsi  17477  dsndxntsetndx  17478  slotsdifdsndx  17479  basendxltunifndx  17483  unifndxntsetndx  17485  slotsdifunifndx  17486  slotsbhcdif  17500  slotsdifocndx  17502  catstr  18049  ipostr  18617  mulgfval  19192  mulg1  19204  mulg2  19206  od1  19686  0subgALT  19695  gex1  19718  efgsval2  19860  efgsp1  19864  torsubg  19981  pgpfaclem1  20210  pmatcollpw3fi1lem2  23012  hauspwdom  23727  imasdsf1olem  24599  cphipval  25471  bcthlem4  25555  bcth3  25559  ovolmge0  25705  ovollb2  25717  ovolctb  25718  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliun  25733  ovoliun2  25734  ovolicc1  25744  voliunlem1  25778  volsup  25784  ioombl1lem2  25787  ioombl1lem4  25789  uniioombllem1  25809  uniioombllem2  25811  uniioombllem6  25816  itg1climres  25942  itg2seq  25970  itg2monolem1  25978  itg2monolem2  25979  itg2monolem3  25980  itg2mono  25981  itg2i1fseq2  25984  itg2cnlem1  25989  aalioulem5  26572  aaliou2b  26577  aaliou3lem4  26582  aaliou3lem7  26585  log2ub  27186  emcllem6  27237  emcllem7  27238  lgam1  27300  gam1  27301  ftalem7  27315  efnnfsumcl  27339  vmaprm  27353  efvmacl  27356  efchtdvds  27395  vma1  27402  prmorcht  27414  sqff1o  27418  pclogsum  27451  perfectlem1  27465  perfectlem2  27466  bpos1  27519  bposlem5  27524  lgsdir  27568  lgs1  27577  lgsquad2lem2  27621  addsqn2reu  27677  addsqrexnreu  27678  dchrmusumlema  27729  dchrisum0lema  27750  slotsinbpsd  28782  slotslnbpsd  28783  trkgstr  28785  angmgmlem  29274  angmgmbas  29277  eengstr  29437  basendxltedgfndx  29451  usgrexmplef  29719  lfgrn1cycl  30273  clwwlkn1  30511  ipval2  31188  opsqrlem2  32622  ssnnssfz  33258  znumd  33283  zdend  33284  nnindf  33290  nn0min  33291  isarchi3  33627  eufndx  33733  eufid  33734  constrext2chnlem  34260  iconstr  34276  rge0scvg  34459  qqh0  34494  qqh1  34495  esumfzf  34579  esumfsup  34580  esumpcvgval  34588  voliune  34740  eulerpartgbij  34883  eulerpartlemgs2  34891  fib2  34913  rrvsum  34965  ballotlem4  35010  ballotlemi1  35014  ballotlemii  35015  ballotlemic  35018  ballotlem1c  35019  hgt750lem  35159  hgt750leme  35166  faclimlem1  36322  nn0prpwlem  36941  nn0prpw  36942  poimirlem32  38401  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  incsequz  38498  bfplem1  38572  rrncmslem  38582  60gcd7e1  42871  12lcm5e60  42874  60lcm7e420  42876  lcm1un  42879  lcmineqlem10  42904  3lexlogpow5ineq1  42920  3lexlogpow5ineq2  42921  aks4d1p1p7  42940  aks6d1c1p8  42981  sticksstones9  43020  sticksstones11  43022  aks6d1c7lem1  43046  3cubes  43535  jm2.23  43837  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  expdioph  43864  relexp2  44517  iunrelexpmin1  44548  iunrelexpmin2  44552  dftrcl3  44560  fvtrcllb1d  44562  cotrcltrcl  44565  corcltrcl  44579  cotrclrcl  44582  prmunb2  45135  sumsnd  45860  nnn0  46207  xrralrecnnge  46219  iooiinicc  46372  iooiinioc  46386  mccl  46428  sumnnodd  46460  wallispilem4  46896  wallispi2lem1  46899  wallispi2lem2  46900  stirlinglem8  46909  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  fourierdlem31  46966  nnfoctbdjlem  47283  hoicvrrex  47384  hoidmvlelem3  47425  ovnhoilem1  47429  ovnhoilem2  47430  ovnlecvr2  47438  ovnsubadd2lem  47473  iinhoiicclem  47501  vonicclem2  47512  numtowerdt  47734  1elfzo1ceilhalf1  48229  iccpartlt  48324  257prm  48464  fmtnoprmfac2lem1  48469  fmtno4prmfac193  48476  fmtno4nprmfac193  48477  fmtno5nprm  48486  3ndvds4  48498  139prmALT  48499  31prm  48500  127prm  48502  3exp4mod41  48519  41prothprmlem2  48521  perfectALTVlem1  48637  perfectALTVlem2  48638  2exp340mod341  48649  341fppr2  48650  4fppr1  48651  nnsum3primesprm  48706  bgoldbtbndlem1  48721  tgblthelfgott  48731  nnsgrpmgm  49091  nnsgrpnmnd  49093  blennn0elnn  49507  blen1  49514  ackval42  49626  1elfz13  50776  veronesevrowd  50812  veronesematrowd  50814  veroquadgsumlem  50816  veroquadmodzerod  50817  veroquadnolindfd  50818