Theorem 1nn 12245

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 11204	. . . 4 ⊢ 1 ∈ V
2		fr0g 8424	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8423	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7886	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7077	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 704	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2860	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12235	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5676	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2786	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2862	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4287   ↦ cmpt 5193  ran crn 5664   ↾ cres 5665   “ cima 5666   Fn wfn 6533  ‘cfv 6538  (class class class)co 7412  ωcom 7863  reccrdg 8397  1c1 11102   + caddc 11104  ℕcn 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  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 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235

This theorem is referenced by:  dfnn2  12247  dfnn3  12248  nnind  12252  nn1suc  12256  nnmulcom  12295  2nn  12315  nnunb  12501  1nn0  12521  nn0p1nn  12544  elz2  12610  1z  12625  neg1z  12631  nneo  12681  9p1e10  12714  11nn  12737  elnn1uz2  12950  zq  12979  rpnnen1lem4  13005  rpnnen1lem5  13006  1elfzo1  13745  ser1const  14096  exp1  14105  nnexpcl  14112  expnbnd  14270  fac1  14315  faccl  14321  faclbnd3  14330  faclbnd4lem1  14331  faclbnd4lem2  14332  faclbnd4lem3  14333  faclbnd4lem4  14334  lsw0  14604  ccat2s1p1  14669  cats1un  14760  revs1  14804  cats1fvn  14897  relexpsucnnl  15069  relexpaddg  15092  isercolllem2  15719  isercolllem3  15720  isercoll  15721  sumsnf  15796  climcndslem1  15905  climcndslem2  15906  fprodnncl  16011  prodsn  16018  prodsnf  16020  nnrisefaccl  16075  eftlub  16166  eirrlem  16261  rpnnen2lem5  16275  rpnnen2lem8  16278  rpnnen2lem12  16282  dvdsle  16369  ndvdsp1  16470  5ndvds6  16473  gcd1  16587  bezoutr1  16628  1nprm  16738  1idssfct  16739  isprm2lem  16740  qden1elz  16817  phi1  16833  phiprm  16837  pcpre1  16903  pczpre  16908  pcmptcl  16952  pcmpt  16953  infpnlem2  16972  prmreclem1  16977  prmreclem6  16982  mul4sq  17015  vdwmc2  17040  vdwlem8  17049  vdwlem13  17054  vdwnnlem3  17058  prmocl  17095  prmop1  17099  fvprmselelfz  17105  fvprmselgcd1  17106  prmolefac  17107  prmodvdslcmf  17108  prmgapprmo  17123  5prm  17169  7prm  17171  10nprm  17174  11prm  17176  13prm  17177  17prm  17178  19prm  17179  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  baseid  17273  basendx  17279  basendxnn  17280  rngstr  17352  lmodstr  17379  topgrpstr  17415  otpsstr  17430  ocndx  17435  ocid  17436  basendxnocndx  17437  plendxnocndx  17438  basendxltdsndx  17442  dsndxnplusgndx  17444  dsndxnmulrndx  17445  slotsdnscsi  17446  dsndxntsetndx  17447  slotsdifdsndx  17448  basendxltunifndx  17452  unifndxntsetndx  17454  slotsdifunifndx  17455  slotsbhcdif  17469  slotsdifocndx  17471  catstr  18018  ipostr  18586  mulgfval  19136  mulg1  19148  mulg2  19150  od1  19630  0subgALT  19639  gex1  19662  efgsval2  19804  efgsp1  19808  torsubg  19925  pgpfaclem1  20154  pmatcollpw3fi1lem2  22925  hauspwdom  23639  imasdsf1olem  24511  cphipval  25383  bcthlem4  25467  bcth3  25471  ovolmge0  25617  ovollb2  25629  ovolctb  25630  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliun  25645  ovoliun2  25646  ovolicc1  25656  voliunlem1  25690  volsup  25696  ioombl1lem2  25699  ioombl1lem4  25701  uniioombllem1  25721  uniioombllem2  25723  uniioombllem6  25728  itg1climres  25854  itg2seq  25882  itg2monolem1  25890  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  itg2i1fseq2  25896  itg2cnlem1  25901  aalioulem5  26480  aaliou2b  26485  aaliou3lem4  26490  aaliou3lem7  26493  log2ub  27095  emcllem6  27146  emcllem7  27147  lgam1  27209  gam1  27210  ftalem7  27224  efnnfsumcl  27248  vmaprm  27262  efvmacl  27265  efchtdvds  27304  vma1  27311  prmorcht  27323  sqff1o  27327  pclogsum  27360  perfectlem1  27374  perfectlem2  27375  bpos1  27428  bposlem5  27433  lgsdir  27477  lgs1  27486  lgsquad2lem2  27530  addsqn2reu  27586  addsqrexnreu  27587  dchrmusumlema  27638  dchrisum0lema  27659  slotsinbpsd  28691  slotslnbpsd  28692  trkgstr  28694  eengstr  29311  basendxltedgfndx  29325  usgrexmplef  29590  lfgrn1cycl  30135  clwwlkn1  30373  ipval2  31040  opsqrlem2  32474  ssnnssfz  33113  znumd  33138  zdend  33139  nnindf  33145  nn0min  33146  isarchi3  33488  eufndx  33594  eufid  33595  constrext2chnlem  34121  iconstr  34137  rge0scvg  34320  qqh0  34355  qqh1  34356  esumfzf  34440  esumfsup  34441  esumpcvgval  34449  voliune  34600  eulerpartgbij  34743  eulerpartlemgs2  34751  fib2  34773  rrvsum  34825  ballotlem4  34870  ballotlemi1  34874  ballotlemii  34875  ballotlemic  34878  ballotlem1c  34879  hgt750lem  35019  hgt750leme  35026  0nn0m1nnn0  35585  faclimlem1  36216  nn0prpwlem  36814  nn0prpw  36815  poimirlem32  38284  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  incsequz  38380  bfplem1  38454  rrncmslem  38464  60gcd7e1  42753  12lcm5e60  42756  60lcm7e420  42758  lcm1un  42761  lcmineqlem10  42786  3lexlogpow5ineq1  42802  3lexlogpow5ineq2  42803  aks4d1p1p7  42822  aks6d1c1p8  42863  sticksstones9  42902  sticksstones11  42904  aks6d1c7lem1  42928  3cubes  43404  jm2.23  43706  rmydioph  43724  rmxdioph  43726  expdiophlem2  43732  expdioph  43733  relexp2  44386  iunrelexpmin1  44417  iunrelexpmin2  44421  dftrcl3  44429  fvtrcllb1d  44431  cotrcltrcl  44434  corcltrcl  44448  cotrclrcl  44451  prmunb2  45004  sumsnd  45729  nnn0  46076  xrralrecnnge  46088  iooiinicc  46241  iooiinioc  46255  mccl  46297  sumnnodd  46329  wallispilem4  46765  wallispi2lem1  46768  wallispi2lem2  46769  stirlinglem8  46778  stirlinglem11  46781  stirlinglem12  46782  stirlinglem13  46783  fourierdlem31  46835  nnfoctbdjlem  47152  hoicvrrex  47253  hoidmvlelem3  47294  ovnhoilem1  47298  ovnhoilem2  47299  ovnlecvr2  47307  ovnsubadd2lem  47342  iinhoiicclem  47370  vonicclem2  47381  nthrucw  47590  1elfzo1ceilhalf1  48061  iccpartlt  48156  257prm  48296  fmtnoprmfac2lem1  48301  fmtno4prmfac193  48308  fmtno4nprmfac193  48309  fmtno5nprm  48318  3ndvds4  48330  139prmALT  48331  31prm  48332  127prm  48334  3exp4mod41  48351  41prothprmlem2  48353  perfectALTVlem1  48469  perfectALTVlem2  48470  2exp340mod341  48481  341fppr2  48482  4fppr1  48483  nnsum3primesprm  48538  bgoldbtbndlem1  48553  tgblthelfgott  48563  nnsgrpmgm  48924  nnsgrpnmnd  48926  blennn0elnn  49340  blen1  49347  ackval42  49459