Theorem 1nn 12136

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 11108	. . . 4 ⊢ 1 ∈ V
2		fr0g 8355	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8354	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7819	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7013	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 692	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2828	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12126	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5629	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2754	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2830	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4283   ↦ cmpt 5172  ran crn 5617   ↾ cres 5618   “ cima 5619   Fn wfn 6476  ‘cfv 6481  (class class class)co 7346  ωcom 7796  reccrdg 8328  1c1 11007   + caddc 11009  ℕcn 12125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126

This theorem is referenced by:  dfnn2  12138  dfnn3  12139  nnind  12143  nn1suc  12147  2nn  12198  nnunb  12377  1nn0  12397  nn0p1nn  12420  elz2  12486  1z  12502  neg1z  12508  nneo  12557  9p1e10  12590  elnn1uz2  12823  zq  12852  rpnnen1lem4  12878  rpnnen1lem5  12879  1elfzo1  13614  ser1const  13965  exp1  13974  nnexpcl  13981  expnbnd  14139  fac1  14184  faccl  14190  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem2  14201  faclbnd4lem3  14202  faclbnd4lem4  14203  lsw0  14472  ccat2s1p1  14537  cats1un  14628  revs1  14672  cats1fvn  14765  relexpsucnnl  14937  relexpaddg  14960  isercolllem2  15573  isercolllem3  15574  isercoll  15575  sumsnf  15650  climcndslem1  15756  climcndslem2  15757  fprodnncl  15862  prodsn  15869  prodsnf  15871  nnrisefaccl  15926  eftlub  16018  eirrlem  16113  rpnnen2lem5  16127  rpnnen2lem8  16130  rpnnen2lem12  16134  dvdsle  16221  ndvdsp1  16322  5ndvds6  16325  gcd1  16439  bezoutr1  16480  1nprm  16590  1idssfct  16591  isprm2lem  16592  qden1elz  16668  phi1  16684  phiprm  16688  pcpre1  16754  pczpre  16759  pcmptcl  16803  pcmpt  16804  infpnlem2  16823  prmreclem1  16828  prmreclem6  16833  mul4sq  16866  vdwmc2  16891  vdwlem8  16900  vdwlem13  16905  vdwnnlem3  16909  prmocl  16946  prmop1  16950  fvprmselelfz  16956  fvprmselgcd1  16957  prmolefac  16958  prmodvdslcmf  16959  prmgapprmo  16974  5prm  17020  7prm  17022  11prm  17026  13prm  17027  17prm  17028  19prm  17029  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  baseid  17123  basendx  17129  basendxnn  17130  rngstr  17202  lmodstr  17229  topgrpstr  17265  otpsstr  17280  ocndx  17285  ocid  17286  basendxnocndx  17287  plendxnocndx  17288  basendxltdsndx  17292  dsndxnplusgndx  17294  dsndxnmulrndx  17295  slotsdnscsi  17296  dsndxntsetndx  17297  slotsdifdsndx  17298  basendxltunifndx  17302  unifndxntsetndx  17304  slotsdifunifndx  17305  slotsbhcdif  17319  slotsdifocndx  17321  catstr  17867  ipostr  18435  mulgfval  18982  mulg1  18994  mulg2  18996  od1  19472  0subgALT  19481  gex1  19504  efgsval2  19646  efgsp1  19650  torsubg  19767  pgpfaclem1  19996  pmatcollpw3fi1lem2  22703  hauspwdom  23417  imasdsf1olem  24289  cphipval  25171  bcthlem4  25255  bcth3  25259  ovolmge0  25406  ovollb2  25418  ovolctb  25419  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun  25434  ovoliun2  25435  ovolicc1  25445  voliunlem1  25479  volsup  25485  ioombl1lem2  25488  ioombl1lem4  25490  uniioombllem1  25510  uniioombllem2  25512  uniioombllem6  25517  itg1climres  25643  itg2seq  25671  itg2monolem1  25679  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2i1fseq2  25685  itg2cnlem1  25690  aalioulem5  26272  aaliou2b  26277  aaliou3lem4  26282  aaliou3lem7  26285  log2ub  26887  emcllem6  26939  emcllem7  26940  lgam1  27002  gam1  27003  ftalem7  27017  efnnfsumcl  27041  vmaprm  27055  efvmacl  27058  efchtdvds  27097  vma1  27104  prmorcht  27116  sqff1o  27120  pclogsum  27154  perfectlem1  27168  perfectlem2  27169  bpos1  27222  bposlem5  27227  lgsdir  27271  lgs1  27280  lgsquad2lem2  27324  addsqn2reu  27380  addsqrexnreu  27381  dchrmusumlema  27432  dchrisum0lema  27453  slotsinbpsd  28420  slotslnbpsd  28421  trkgstr  28423  eengstr  28959  basendxltedgfndx  28973  usgrexmplef  29238  lfgrn1cycl  29784  clwwlkn1  30019  ipval2  30685  opsqrlem2  32119  ssnnssfz  32768  znumd  32793  zdend  32794  nnindf  32800  nn0min  32801  isarchi3  33154  eufndx  33254  eufid  33255  constrext2chnlem  33761  iconstr  33777  rge0scvg  33960  qqh0  33995  qqh1  33996  esumfzf  34080  esumfsup  34081  esumpcvgval  34089  voliune  34240  eulerpartgbij  34383  eulerpartlemgs2  34391  fib2  34413  rrvsum  34465  ballotlem4  34510  ballotlemi1  34514  ballotlemii  34515  ballotlemic  34518  ballotlem1c  34519  hgt750lem  34662  hgt750leme  34669  0nn0m1nnn0  35155  faclimlem1  35785  nn0prpwlem  36362  nn0prpw  36363  poimirlem32  37698  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  incsequz  37794  bfplem1  37868  rrncmslem  37878  60gcd7e1  42044  12lcm5e60  42047  60lcm7e420  42049  lcm1un  42052  lcmineqlem10  42077  3lexlogpow5ineq1  42093  3lexlogpow5ineq2  42094  3lexlogpow5ineq4  42095  aks4d1p1p7  42113  aks6d1c1p8  42154  sticksstones9  42193  sticksstones11  42195  aks6d1c7lem1  42219  nnmulcom  42311  3cubes  42729  jm2.23  43035  rmydioph  43053  rmxdioph  43055  expdiophlem2  43061  expdioph  43062  relexp2  43716  iunrelexpmin1  43747  iunrelexpmin2  43751  dftrcl3  43759  fvtrcllb1d  43761  cotrcltrcl  43764  corcltrcl  43778  cotrclrcl  43781  prmunb2  44350  sumsnd  45069  nnn0  45422  xrralrecnnge  45434  iooiinicc  45588  iooiinioc  45602  mccl  45644  sumnnodd  45676  wallispilem4  46112  wallispi2lem1  46115  wallispi2lem2  46116  stirlinglem8  46125  stirlinglem11  46128  stirlinglem12  46129  stirlinglem13  46130  fourierdlem31  46182  nnfoctbdjlem  46499  hoicvr  46592  hoicvrrex  46600  hoidmvlelem3  46641  ovnhoilem1  46645  ovnhoilem2  46646  ovnlecvr2  46654  ovnsubadd2lem  46689  iinhoiicclem  46717  vonicclem2  46728  1elfzo1ceilhalf1  47374  iccpartlt  47461  257prm  47598  fmtnoprmfac2lem1  47603  fmtno4prmfac193  47610  fmtno4nprmfac193  47611  fmtno5nprm  47620  3ndvds4  47632  139prmALT  47633  31prm  47634  127prm  47636  3exp4mod41  47653  41prothprmlem2  47655  perfectALTVlem1  47758  perfectALTVlem2  47759  2exp340mod341  47770  341fppr2  47771  4fppr1  47772  nnsum3primesprm  47827  bgoldbtbndlem1  47842  tgblthelfgott  47852  nnsgrpmgm  48213  nnsgrpnmnd  48215  blennn0elnn  48615  blen1  48622  ackval42  48734