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 8368	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8367	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7833	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7026	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 693	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2834	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12166	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5637	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2760	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2836	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274   ↦ cmpt 5167  ran crn 5625   ↾ cres 5626   “ cima 5627   Fn wfn 6487  ‘cfv 6492  (class class class)co 7360  ωcom 7810  reccrdg 8341  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  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  22762  hauspwdom  23476  imasdsf1olem  24348  cphipval  25220  bcthlem4  25304  bcth3  25308  ovolmge0  25454  ovollb2  25466  ovolctb  25467  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliun  25482  ovoliun2  25483  ovolicc1  25493  voliunlem1  25527  volsup  25533  ioombl1lem2  25536  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem2  25560  uniioombllem6  25565  itg1climres  25691  itg2seq  25719  itg2monolem1  25727  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2i1fseq2  25733  itg2cnlem1  25738  aalioulem5  26313  aaliou2b  26318  aaliou3lem4  26323  aaliou3lem7  26326  log2ub  26926  emcllem6  26978  emcllem7  26979  lgam1  27041  gam1  27042  ftalem7  27056  efnnfsumcl  27080  vmaprm  27094  efvmacl  27097  efchtdvds  27136  vma1  27143  prmorcht  27155  sqff1o  27159  pclogsum  27192  perfectlem1  27206  perfectlem2  27207  bpos1  27260  bposlem5  27265  lgsdir  27309  lgs1  27318  lgsquad2lem2  27362  addsqn2reu  27418  addsqrexnreu  27419  dchrmusumlema  27470  dchrisum0lema  27491  slotsinbpsd  28523  slotslnbpsd  28524  trkgstr  28526  eengstr  29063  basendxltedgfndx  29077  usgrexmplef  29342  lfgrn1cycl  29888  clwwlkn1  30126  ipval2  30793  opsqrlem2  32227  ssnnssfz  32875  znumd  32901  zdend  32902  nnindf  32908  nn0min  32909  isarchi3  33263  eufndx  33366  eufid  33367  constrext2chnlem  33910  iconstr  33926  rge0scvg  34109  qqh0  34144  qqh1  34145  esumfzf  34229  esumfsup  34230  esumpcvgval  34238  voliune  34389  eulerpartgbij  34532  eulerpartlemgs2  34540  fib2  34562  rrvsum  34614  ballotlem4  34659  ballotlemi1  34663  ballotlemii  34664  ballotlemic  34667  ballotlem1c  34668  hgt750lem  34811  hgt750leme  34818  0nn0m1nnn0  35311  faclimlem1  35941  nn0prpwlem  36520  nn0prpw  36521  poimirlem32  37987  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  incsequz  38083  bfplem1  38157  rrncmslem  38167  60gcd7e1  42458  12lcm5e60  42461  60lcm7e420  42463  lcm1un  42466  lcmineqlem10  42491  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  aks4d1p1p7  42527  aks6d1c1p8  42568  sticksstones9  42607  sticksstones11  42609  aks6d1c7lem1  42633  3cubes  43136  jm2.23  43442  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  relexp2  44122  iunrelexpmin1  44153  iunrelexpmin2  44157  dftrcl3  44165  fvtrcllb1d  44167  cotrcltrcl  44170  corcltrcl  44184  cotrclrcl  44187  prmunb2  44756  sumsnd  45475  nnn0  45825  xrralrecnnge  45837  iooiinicc  45990  iooiinioc  46004  mccl  46046  sumnnodd  46078  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem8  46527  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  fourierdlem31  46584  nnfoctbdjlem  46901  hoicvrrex  47002  hoidmvlelem3  47043  ovnhoilem1  47047  ovnhoilem2  47048  ovnlecvr2  47056  ovnsubadd2lem  47091  iinhoiicclem  47119  vonicclem2  47130  nthrucw  47332  1elfzo1ceilhalf1  47801  iccpartlt  47896  257prm  48036  fmtnoprmfac2lem1  48041  fmtno4prmfac193  48048  fmtno4nprmfac193  48049  fmtno5nprm  48058  3ndvds4  48070  139prmALT  48071  31prm  48072  127prm  48074  3exp4mod41  48091  41prothprmlem2  48093  perfectALTVlem1  48209  perfectALTVlem2  48210  2exp340mod341  48221  341fppr2  48222  4fppr1  48223  nnsum3primesprm  48278  bgoldbtbndlem1  48293  tgblthelfgott  48303  nnsgrpmgm  48664  nnsgrpnmnd  48666  blennn0elnn  49065  blen1  49072  ackval42  49184