Theorem 1nn 12240

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 11199	. . . 4 ⊢ 1 ∈ V
2		fr0g 8419	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8418	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7881	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7073	. . . 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 2866	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12230	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5672	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2792	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2868	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ∅c0 4294   ↦ cmpt 5193  ran crn 5660   ↾ cres 5661   “ cima 5662   Fn wfn 6528  ‘cfv 6533  (class class class)co 7408  ωcom 7858  reccrdg 8392  1c1 11097   + caddc 11099  ℕcn 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12230

This theorem is referenced by:  dfnn2  12242  dfnn3  12243  nnind  12247  nn1suc  12251  nnmulcom  12290  2nn  12310  nnunb  12496  1nn0  12516  nn0p1nn  12539  elz2  12605  1z  12620  neg1z  12626  nneo  12676  9p1e10  12709  11nn  12732  elnn1uz2  12945  zq  12974  rpnnen1lem4  13000  rpnnen1lem5  13001  1elfzo1  13739  ser1const  14090  exp1  14099  nnexpcl  14106  expnbnd  14264  fac1  14309  faccl  14315  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem2  14326  faclbnd4lem3  14327  faclbnd4lem4  14328  lsw0  14598  ccat2s1p1  14663  cats1un  14754  revs1  14798  cats1fvn  14891  relexpsucnnl  15063  relexpaddg  15086  isercolllem2  15713  isercolllem3  15714  isercoll  15715  sumsnf  15790  climcndslem1  15899  climcndslem2  15900  fprodnncl  16005  prodsn  16012  prodsnf  16014  nnrisefaccl  16069  eftlub  16161  eirrlem  16256  rpnnen2lem5  16270  rpnnen2lem8  16273  rpnnen2lem12  16277  dvdsle  16364  ndvdsp1  16465  5ndvds6  16468  gcd1  16582  bezoutr1  16623  1nprm  16733  1idssfct  16734  isprm2lem  16735  qden1elz  16812  phi1  16828  phiprm  16832  pcpre1  16898  pczpre  16903  pcmptcl  16947  pcmpt  16948  infpnlem2  16967  prmreclem1  16972  prmreclem6  16977  mul4sq  17010  vdwmc2  17035  vdwlem8  17044  vdwlem13  17049  vdwnnlem3  17053  prmocl  17090  prmop1  17094  fvprmselelfz  17100  fvprmselgcd1  17101  prmolefac  17102  prmodvdslcmf  17103  prmgapprmo  17118  5prm  17164  7prm  17166  10nprm  17169  11prm  17171  13prm  17172  17prm  17173  19prm  17174  37prm  17177  43prm  17178  83prm  17179  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem4  17190  1259lem5  17191  1259prm  17192  2503lem3  17195  2503prm  17196  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  4001prm  17201  baseid  17268  basendx  17274  basendxnn  17275  rngstr  17347  lmodstr  17374  topgrpstr  17410  otpsstr  17425  ocndx  17430  ocid  17431  basendxnocndx  17432  plendxnocndx  17433  basendxltdsndx  17437  dsndxnplusgndx  17439  dsndxnmulrndx  17440  slotsdnscsi  17441  dsndxntsetndx  17442  slotsdifdsndx  17443  basendxltunifndx  17447  unifndxntsetndx  17449  slotsdifunifndx  17450  slotsbhcdif  17464  slotsdifocndx  17466  catstr  18013  ipostr  18581  mulgfval  19131  mulg1  19143  mulg2  19145  od1  19625  0subgALT  19634  gex1  19657  efgsval2  19799  efgsp1  19803  torsubg  19920  pgpfaclem1  20149  pmatcollpw3fi1lem2  22909  hauspwdom  23623  imasdsf1olem  24495  cphipval  25367  bcthlem4  25451  bcth3  25455  ovolmge0  25601  ovollb2  25613  ovolctb  25614  ovolunlem1a  25620  ovolunlem1  25621  ovoliunlem1  25626  ovoliun  25629  ovoliun2  25630  ovolicc1  25640  voliunlem1  25674  volsup  25680  ioombl1lem2  25683  ioombl1lem4  25685  uniioombllem1  25705  uniioombllem2  25707  uniioombllem6  25712  itg1climres  25838  itg2seq  25866  itg2monolem1  25874  itg2monolem2  25875  itg2monolem3  25876  itg2mono  25877  itg2i1fseq2  25880  itg2cnlem1  25885  aalioulem5  26462  aaliou2b  26467  aaliou3lem4  26472  aaliou3lem7  26475  log2ub  27076  emcllem6  27127  emcllem7  27128  lgam1  27190  gam1  27191  ftalem7  27205  efnnfsumcl  27229  vmaprm  27243  efvmacl  27246  efchtdvds  27285  vma1  27292  prmorcht  27304  sqff1o  27308  pclogsum  27341  perfectlem1  27355  perfectlem2  27356  bpos1  27409  bposlem5  27414  lgsdir  27458  lgs1  27467  lgsquad2lem2  27511  addsqn2reu  27567  addsqrexnreu  27568  dchrmusumlema  27619  dchrisum0lema  27640  slotsinbpsd  28672  slotslnbpsd  28673  trkgstr  28675  eengstr  29267  basendxltedgfndx  29281  usgrexmplef  29546  lfgrn1cycl  30091  clwwlkn1  30329  ipval2  30996  opsqrlem2  32430  ssnnssfz  33069  znumd  33094  zdend  33095  nnindf  33101  nn0min  33102  isarchi3  33444  eufndx  33550  eufid  33551  constrext2chnlem  34081  iconstr  34097  rge0scvg  34280  qqh0  34315  qqh1  34316  esumfzf  34400  esumfsup  34401  esumpcvgval  34409  voliune  34560  eulerpartgbij  34703  eulerpartlemgs2  34711  fib2  34733  rrvsum  34785  ballotlem4  34830  ballotlemi1  34834  ballotlemii  34835  ballotlemic  34838  ballotlem1c  34839  hgt750lem  34979  hgt750leme  34986  0nn0m1nnn0  35499  faclimlem1  36130  nn0prpwlem  36718  nn0prpw  36719  poimirlem32  38186  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  incsequz  38282  bfplem1  38356  rrncmslem  38366  60gcd7e1  42657  12lcm5e60  42660  60lcm7e420  42662  lcm1un  42665  lcmineqlem10  42690  3lexlogpow5ineq1  42706  3lexlogpow5ineq2  42707  aks4d1p1p7  42726  aks6d1c1p8  42767  sticksstones9  42806  sticksstones11  42808  aks6d1c7lem1  42832  3cubes  43306  jm2.23  43608  rmydioph  43626  rmxdioph  43628  expdiophlem2  43634  expdioph  43635  relexp2  44288  iunrelexpmin1  44319  iunrelexpmin2  44323  dftrcl3  44331  fvtrcllb1d  44333  cotrcltrcl  44336  corcltrcl  44350  cotrclrcl  44353  prmunb2  44906  sumsnd  45631  nnn0  45978  xrralrecnnge  45990  iooiinicc  46143  iooiinioc  46157  mccl  46199  sumnnodd  46231  wallispilem4  46667  wallispi2lem1  46670  wallispi2lem2  46671  stirlinglem8  46680  stirlinglem11  46683  stirlinglem12  46684  stirlinglem13  46685  fourierdlem31  46737  nnfoctbdjlem  47054  hoicvrrex  47155  hoidmvlelem3  47196  ovnhoilem1  47200  ovnhoilem2  47201  ovnlecvr2  47209  ovnsubadd2lem  47244  iinhoiicclem  47272  vonicclem2  47283  nthrucw  47487  1elfzo1ceilhalf1  47960  iccpartlt  48055  257prm  48195  fmtnoprmfac2lem1  48200  fmtno4prmfac193  48207  fmtno4nprmfac193  48208  fmtno5nprm  48217  3ndvds4  48229  139prmALT  48230  31prm  48231  127prm  48233  3exp4mod41  48250  41prothprmlem2  48252  perfectALTVlem1  48368  perfectALTVlem2  48369  2exp340mod341  48380  341fppr2  48381  4fppr1  48382  nnsum3primesprm  48437  bgoldbtbndlem1  48452  tgblthelfgott  48462  nnsgrpmgm  48823  nnsgrpnmnd  48825  blennn0elnn  49235  blen1  49242  ackval42  49354