Theorem 1nn 12255

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 11214	. . . 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 7887	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7079	. . . 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 2862	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12245	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5676	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2788	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2864	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  ∅c0 4286   ↦ cmpt 5194  ran crn 5664   ↾ cres 5665   “ cima 5666   Fn wfn 6535  ‘cfv 6540  (class class class)co 7416  ωcom 7864  reccrdg 8398  1c1 11112   + caddc 11114  ℕcn 12244

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12245

This theorem is used by:  dfnn2  12257  dfnn3  12258  nnind  12262  nn1suc  12266  nnmulcom  12305  2nn  12325  nnunb  12511  1nn0  12531  nn0p1nn  12554  elz2  12620  1z  12635  neg1z  12641  nneo  12691  9p1e10  12724  11nn  12747  elnn1uz2  12960  zq  12989  rpnnen1lem4  13015  rpnnen1lem5  13016  1elfzo1  13755  ser1const  14107  exp1  14116  nnexpcl  14123  expnbnd  14281  fac1  14326  faccl  14332  faclbnd3  14341  faclbnd4lem1  14342  faclbnd4lem2  14343  faclbnd4lem3  14344  faclbnd4lem4  14345  lsw0  14615  ccat2s1p1  14682  cats1un  14775  revs1  14819  cats1fvn  14914  relexpsucnnl  15086  relexpaddg  15109  isercolllem2  15736  isercolllem3  15737  isercoll  15738  sumsnf  15812  climcndslem1  15921  climcndslem2  15922  fprodnncl  16027  prodsn  16034  prodsnf  16036  nnrisefaccl  16091  eftlub  16182  eirrlem  16277  rpnnen2lem5  16291  rpnnen2lem8  16294  rpnnen2lem12  16298  dvdsle  16385  ndvdsp1  16486  5ndvds6  16489  gcd1  16603  bezoutr1  16644  1nprm  16754  1idssfct  16755  isprm2lem  16756  qden1elz  16833  phi1  16849  phiprm  16853  pcpre1  16919  pczpre  16924  pcmptcl  16968  pcmpt  16969  infpnlem2  16988  prmreclem1  16993  prmreclem6  16998  mul4sq  17031  vdwmc2  17056  vdwlem8  17065  vdwlem13  17070  vdwnnlem3  17074  prmocl  17111  prmop1  17115  fvprmselelfz  17121  fvprmselgcd1  17122  prmolefac  17123  prmodvdslcmf  17124  prmgapprmo  17139  5prm  17185  7prm  17187  10nprm  17190  11prm  17192  13prm  17193  17prm  17194  19prm  17195  37prm  17198  43prm  17199  83prm  17200  139prm  17201  163prm  17202  317prm  17203  631prm  17204  1259lem4  17211  1259lem5  17212  1259prm  17213  2503lem3  17216  2503prm  17217  4001lem1  17218  4001lem2  17219  4001lem3  17220  4001lem4  17221  4001prm  17222  baseid  17289  basendx  17295  basendxnn  17296  rngstr  17368  lmodstr  17395  topgrpstr  17431  otpsstr  17446  ocndx  17451  ocid  17452  basendxnocndx  17453  plendxnocndx  17454  basendxltdsndx  17458  dsndxnplusgndx  17460  dsndxnmulrndx  17461  slotsdnscsi  17462  dsndxntsetndx  17463  slotsdifdsndx  17464  basendxltunifndx  17468  unifndxntsetndx  17470  slotsdifunifndx  17471  slotsbhcdif  17485  slotsdifocndx  17487  catstr  18034  ipostr  18602  mulgfval  19158  mulg1  19170  mulg2  19172  od1  19652  0subgALT  19661  gex1  19684  efgsval2  19826  efgsp1  19830  torsubg  19947  pgpfaclem1  20176  pmatcollpw3fi1lem2  22973  hauspwdom  23687  imasdsf1olem  24559  cphipval  25431  bcthlem4  25515  bcth3  25519  ovolmge0  25665  ovollb2  25677  ovolctb  25678  ovolunlem1a  25684  ovolunlem1  25685  ovoliunlem1  25690  ovoliun  25693  ovoliun2  25694  ovolicc1  25704  voliunlem1  25738  volsup  25744  ioombl1lem2  25747  ioombl1lem4  25749  uniioombllem1  25769  uniioombllem2  25771  uniioombllem6  25776  itg1climres  25902  itg2seq  25930  itg2monolem1  25938  itg2monolem2  25939  itg2monolem3  25940  itg2mono  25941  itg2i1fseq2  25944  itg2cnlem1  25949  aalioulem5  26528  aaliou2b  26533  aaliou3lem4  26538  aaliou3lem7  26541  log2ub  27143  emcllem6  27194  emcllem7  27195  lgam1  27257  gam1  27258  ftalem7  27272  efnnfsumcl  27296  vmaprm  27310  efvmacl  27313  efchtdvds  27352  vma1  27359  prmorcht  27371  sqff1o  27375  pclogsum  27408  perfectlem1  27422  perfectlem2  27423  bpos1  27476  bposlem5  27481  lgsdir  27525  lgs1  27534  lgsquad2lem2  27578  addsqn2reu  27634  addsqrexnreu  27635  dchrmusumlema  27686  dchrisum0lema  27707  slotsinbpsd  28739  slotslnbpsd  28740  trkgstr  28742  eengstr  29359  basendxltedgfndx  29373  usgrexmplef  29638  lfgrn1cycl  30183  clwwlkn1  30421  ipval2  31088  opsqrlem2  32522  ssnnssfz  33161  znumd  33186  zdend  33187  nnindf  33193  nn0min  33194  isarchi3  33530  eufndx  33636  eufid  33637  constrext2chnlem  34163  iconstr  34179  rge0scvg  34362  qqh0  34397  qqh1  34398  esumfzf  34482  esumfsup  34483  esumpcvgval  34491  voliune  34643  eulerpartgbij  34786  eulerpartlemgs2  34794  fib2  34816  rrvsum  34868  ballotlem4  34913  ballotlemi1  34917  ballotlemii  34918  ballotlemic  34921  ballotlem1c  34922  hgt750lem  35062  hgt750leme  35069  0nn0m1nnn0  35620  faclimlem1  36248  nn0prpwlem  36866  nn0prpw  36867  poimirlem32  38336  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  incsequz  38432  bfplem1  38506  rrncmslem  38516  60gcd7e1  42805  12lcm5e60  42808  60lcm7e420  42810  lcm1un  42813  lcmineqlem10  42838  3lexlogpow5ineq1  42854  3lexlogpow5ineq2  42855  aks4d1p1p7  42874  aks6d1c1p8  42915  sticksstones9  42954  sticksstones11  42956  aks6d1c7lem1  42980  3cubes  43454  jm2.23  43756  rmydioph  43774  rmxdioph  43776  expdiophlem2  43782  expdioph  43783  relexp2  44436  iunrelexpmin1  44467  iunrelexpmin2  44471  dftrcl3  44479  fvtrcllb1d  44481  cotrcltrcl  44484  corcltrcl  44498  cotrclrcl  44501  prmunb2  45054  sumsnd  45779  nnn0  46126  xrralrecnnge  46138  iooiinicc  46291  iooiinioc  46305  mccl  46347  sumnnodd  46379  wallispilem4  46815  wallispi2lem1  46818  wallispi2lem2  46819  stirlinglem8  46828  stirlinglem11  46831  stirlinglem12  46832  stirlinglem13  46833  fourierdlem31  46885  nnfoctbdjlem  47202  hoicvrrex  47303  hoidmvlelem3  47344  ovnhoilem1  47348  ovnhoilem2  47349  ovnlecvr2  47357  ovnsubadd2lem  47392  iinhoiicclem  47420  vonicclem2  47431  nthrucw  47640  1elfzo1ceilhalf1  48111  iccpartlt  48206  257prm  48346  fmtnoprmfac2lem1  48351  fmtno4prmfac193  48358  fmtno4nprmfac193  48359  fmtno5nprm  48368  3ndvds4  48380  139prmALT  48381  31prm  48382  127prm  48384  3exp4mod41  48401  41prothprmlem2  48403  perfectALTVlem1  48519  perfectALTVlem2  48520  2exp340mod341  48531  341fppr2  48532  4fppr1  48533  nnsum3primesprm  48588  bgoldbtbndlem1  48603  tgblthelfgott  48613  nnsgrpmgm  48974  nnsgrpnmnd  48976  blennn0elnn  49390  blen1  49397  ackval42  49509