Theorem 1nn 12176

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 11131	. . . 4 ⊢ 1 ∈ V
2		fr0g 8365	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8364	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7829	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7021	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 698	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2836	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12166	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5631	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2762	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2838	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261   ↦ cmpt 5153  ran crn 5619   ↾ cres 5620   “ cima 5621   Fn wfn 6480  ‘cfv 6485  (class class class)co 7356  ωcom 7806  reccrdg 8338  1c1 11030   + caddc 11032  ℕcn 12165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166

This theorem is referenced by:  dfnn2  12178  dfnn3  12179  nnind  12183  nn1suc  12187  nnmulcom  12226  2nn  12245  nnunb  12424  1nn0  12444  nn0p1nn  12467  elz2  12533  1z  12548  neg1z  12554  nneo  12604  9p1e10  12637  elnn1uz2  12866  zq  12895  rpnnen1lem4  12921  rpnnen1lem5  12922  1elfzo1  13660  ser1const  14011  exp1  14020  nnexpcl  14027  expnbnd  14185  fac1  14230  faccl  14236  faclbnd3  14245  faclbnd4lem1  14246  faclbnd4lem2  14247  faclbnd4lem3  14248  faclbnd4lem4  14249  lsw0  14518  ccat2s1p1  14583  cats1un  14674  revs1  14718  cats1fvn  14811  relexpsucnnl  14983  relexpaddg  15006  isercolllem2  15619  isercolllem3  15620  isercoll  15621  sumsnf  15696  climcndslem1  15805  climcndslem2  15806  fprodnncl  15911  prodsn  15918  prodsnf  15920  nnrisefaccl  15975  eftlub  16067  eirrlem  16162  rpnnen2lem5  16176  rpnnen2lem8  16179  rpnnen2lem12  16183  dvdsle  16270  ndvdsp1  16371  5ndvds6  16374  gcd1  16488  bezoutr1  16529  1nprm  16639  1idssfct  16640  isprm2lem  16641  qden1elz  16718  phi1  16734  phiprm  16738  pcpre1  16804  pczpre  16809  pcmptcl  16853  pcmpt  16854  infpnlem2  16873  prmreclem1  16878  prmreclem6  16883  mul4sq  16916  vdwmc2  16941  vdwlem8  16950  vdwlem13  16955  vdwnnlem3  16959  prmocl  16996  prmop1  17000  fvprmselelfz  17006  fvprmselgcd1  17007  prmolefac  17008  prmodvdslcmf  17009  prmgapprmo  17024  5prm  17070  7prm  17072  11prm  17076  13prm  17077  17prm  17078  19prm  17079  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  baseid  17173  basendx  17179  basendxnn  17180  rngstr  17252  lmodstr  17279  topgrpstr  17315  otpsstr  17330  ocndx  17335  ocid  17336  basendxnocndx  17337  plendxnocndx  17338  basendxltdsndx  17342  dsndxnplusgndx  17344  dsndxnmulrndx  17345  slotsdnscsi  17346  dsndxntsetndx  17347  slotsdifdsndx  17348  basendxltunifndx  17352  unifndxntsetndx  17354  slotsdifunifndx  17355  slotsbhcdif  17369  slotsdifocndx  17371  catstr  17918  ipostr  18486  mulgfval  19036  mulg1  19048  mulg2  19050  od1  19525  0subgALT  19534  gex1  19557  efgsval2  19699  efgsp1  19703  torsubg  19820  pgpfaclem1  20049  pmatcollpw3fi1lem2  22770  hauspwdom  23484  imasdsf1olem  24356  cphipval  25228  bcthlem4  25312  bcth3  25316  ovolmge0  25462  ovollb2  25474  ovolctb  25475  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliun  25490  ovoliun2  25491  ovolicc1  25501  voliunlem1  25535  volsup  25541  ioombl1lem2  25544  ioombl1lem4  25546  uniioombllem1  25566  uniioombllem2  25568  uniioombllem6  25573  itg1climres  25699  itg2seq  25727  itg2monolem1  25735  itg2monolem2  25736  itg2monolem3  25737  itg2mono  25738  itg2i1fseq2  25741  itg2cnlem1  25746  aalioulem5  26320  aaliou2b  26325  aaliou3lem4  26330  aaliou3lem7  26333  log2ub  26931  emcllem6  26982  emcllem7  26983  lgam1  27045  gam1  27046  ftalem7  27060  efnnfsumcl  27084  vmaprm  27098  efvmacl  27101  efchtdvds  27140  vma1  27147  prmorcht  27159  sqff1o  27163  pclogsum  27196  perfectlem1  27210  perfectlem2  27211  bpos1  27264  bposlem5  27269  lgsdir  27313  lgs1  27322  lgsquad2lem2  27366  addsqn2reu  27422  addsqrexnreu  27423  dchrmusumlema  27474  dchrisum0lema  27495  slotsinbpsd  28527  slotslnbpsd  28528  trkgstr  28530  eengstr  29067  basendxltedgfndx  29081  usgrexmplef  29346  lfgrn1cycl  29891  clwwlkn1  30129  ipval2  30796  opsqrlem2  32230  ssnnssfz  32879  znumd  32905  zdend  32906  nnindf  32912  nn0min  32913  isarchi3  33268  eufndx  33374  eufid  33375  constrext2chnlem  33934  iconstr  33950  rge0scvg  34133  qqh0  34168  qqh1  34169  esumfzf  34253  esumfsup  34254  esumpcvgval  34262  voliune  34413  eulerpartgbij  34556  eulerpartlemgs2  34564  fib2  34586  rrvsum  34638  ballotlem4  34683  ballotlemi1  34687  ballotlemii  34688  ballotlemic  34691  ballotlem1c  34692  hgt750lem  34835  hgt750leme  34842  0nn0m1nnn0  35341  faclimlem1  35971  nn0prpwlem  36550  nn0prpw  36551  poimirlem32  38019  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  incsequz  38115  bfplem1  38189  rrncmslem  38199  60gcd7e1  42490  12lcm5e60  42493  60lcm7e420  42495  lcm1un  42498  lcmineqlem10  42523  3lexlogpow5ineq1  42539  3lexlogpow5ineq2  42540  3lexlogpow5ineq4  42541  aks4d1p1p7  42559  aks6d1c1p8  42600  sticksstones9  42639  sticksstones11  42641  aks6d1c7lem1  42665  3cubes  43139  jm2.23  43441  rmydioph  43459  rmxdioph  43461  expdiophlem2  43467  expdioph  43468  relexp2  44121  iunrelexpmin1  44152  iunrelexpmin2  44156  dftrcl3  44164  fvtrcllb1d  44166  cotrcltrcl  44169  corcltrcl  44183  cotrclrcl  44186  prmunb2  44755  sumsnd  45474  nnn0  45822  xrralrecnnge  45834  iooiinicc  45987  iooiinioc  46001  mccl  46043  sumnnodd  46075  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem8  46524  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  fourierdlem31  46581  nnfoctbdjlem  46898  hoicvrrex  46999  hoidmvlelem3  47040  ovnhoilem1  47044  ovnhoilem2  47045  ovnlecvr2  47053  ovnsubadd2lem  47088  iinhoiicclem  47116  vonicclem2  47127  nthrucw  47331  1elfzo1ceilhalf1  47804  iccpartlt  47899  257prm  48039  fmtnoprmfac2lem1  48044  fmtno4prmfac193  48051  fmtno4nprmfac193  48052  fmtno5nprm  48061  3ndvds4  48073  139prmALT  48074  31prm  48075  127prm  48077  3exp4mod41  48094  41prothprmlem2  48096  perfectALTVlem1  48212  perfectALTVlem2  48213  2exp340mod341  48224  341fppr2  48225  4fppr1  48226  nnsum3primesprm  48281  bgoldbtbndlem1  48296  tgblthelfgott  48306  nnsgrpmgm  48667  nnsgrpnmnd  48669  blennn0elnn  49068  blen1  49075  ackval42  49187