Theorem 1nn 12185

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 11140	. . . 4 ⊢ 1 ∈ V
2		fr0g 8375	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8374	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7840	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7032	. . . 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 2833	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12175	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5644	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2759	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2835	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273   ↦ cmpt 5166  ran crn 5632   ↾ cres 5633   “ cima 5634   Fn wfn 6493  ‘cfv 6498  (class class class)co 7367  ωcom 7817  reccrdg 8348  1c1 11039   + caddc 11041  ℕcn 12174

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175

This theorem is referenced by:  dfnn2  12187  dfnn3  12188  nnind  12192  nn1suc  12196  nnmulcom  12235  2nn  12254  nnunb  12433  1nn0  12453  nn0p1nn  12476  elz2  12542  1z  12557  neg1z  12563  nneo  12613  9p1e10  12646  elnn1uz2  12875  zq  12904  rpnnen1lem4  12930  rpnnen1lem5  12931  1elfzo1  13669  ser1const  14020  exp1  14029  nnexpcl  14036  expnbnd  14194  fac1  14239  faccl  14245  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem2  14256  faclbnd4lem3  14257  faclbnd4lem4  14258  lsw0  14527  ccat2s1p1  14592  cats1un  14683  revs1  14727  cats1fvn  14820  relexpsucnnl  14992  relexpaddg  15015  isercolllem2  15628  isercolllem3  15629  isercoll  15630  sumsnf  15705  climcndslem1  15814  climcndslem2  15815  fprodnncl  15920  prodsn  15927  prodsnf  15929  nnrisefaccl  15984  eftlub  16076  eirrlem  16171  rpnnen2lem5  16185  rpnnen2lem8  16188  rpnnen2lem12  16192  dvdsle  16279  ndvdsp1  16380  5ndvds6  16383  gcd1  16497  bezoutr1  16538  1nprm  16648  1idssfct  16649  isprm2lem  16650  qden1elz  16727  phi1  16743  phiprm  16747  pcpre1  16813  pczpre  16818  pcmptcl  16862  pcmpt  16863  infpnlem2  16882  prmreclem1  16887  prmreclem6  16892  mul4sq  16925  vdwmc2  16950  vdwlem8  16959  vdwlem13  16964  vdwnnlem3  16968  prmocl  17005  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  prmolefac  17017  prmodvdslcmf  17018  prmgapprmo  17033  5prm  17079  7prm  17081  11prm  17085  13prm  17086  17prm  17087  19prm  17088  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  baseid  17182  basendx  17188  basendxnn  17189  rngstr  17261  lmodstr  17288  topgrpstr  17324  otpsstr  17339  ocndx  17344  ocid  17345  basendxnocndx  17346  plendxnocndx  17347  basendxltdsndx  17351  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  basendxltunifndx  17361  unifndxntsetndx  17363  slotsdifunifndx  17364  slotsbhcdif  17378  slotsdifocndx  17380  catstr  17927  ipostr  18495  mulgfval  19045  mulg1  19057  mulg2  19059  od1  19534  0subgALT  19543  gex1  19566  efgsval2  19708  efgsp1  19712  torsubg  19829  pgpfaclem1  20058  pmatcollpw3fi1lem2  22752  hauspwdom  23466  imasdsf1olem  24338  cphipval  25210  bcthlem4  25294  bcth3  25298  ovolmge0  25444  ovollb2  25456  ovolctb  25457  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun  25472  ovoliun2  25473  ovolicc1  25483  voliunlem1  25517  volsup  25523  ioombl1lem2  25526  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  itg1climres  25681  itg2seq  25709  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2i1fseq2  25723  itg2cnlem1  25728  aalioulem5  26302  aaliou2b  26307  aaliou3lem4  26312  aaliou3lem7  26315  log2ub  26913  emcllem6  26964  emcllem7  26965  lgam1  27027  gam1  27028  ftalem7  27042  efnnfsumcl  27066  vmaprm  27080  efvmacl  27083  efchtdvds  27122  vma1  27129  prmorcht  27141  sqff1o  27145  pclogsum  27178  perfectlem1  27192  perfectlem2  27193  bpos1  27246  bposlem5  27251  lgsdir  27295  lgs1  27304  lgsquad2lem2  27348  addsqn2reu  27404  addsqrexnreu  27405  dchrmusumlema  27456  dchrisum0lema  27477  slotsinbpsd  28509  slotslnbpsd  28510  trkgstr  28512  eengstr  29049  basendxltedgfndx  29063  usgrexmplef  29328  lfgrn1cycl  29873  clwwlkn1  30111  ipval2  30778  opsqrlem2  32212  ssnnssfz  32860  znumd  32886  zdend  32887  nnindf  32893  nn0min  32894  isarchi3  33248  eufndx  33351  eufid  33352  constrext2chnlem  33894  iconstr  33910  rge0scvg  34093  qqh0  34128  qqh1  34129  esumfzf  34213  esumfsup  34214  esumpcvgval  34222  voliune  34373  eulerpartgbij  34516  eulerpartlemgs2  34524  fib2  34546  rrvsum  34598  ballotlem4  34643  ballotlemi1  34647  ballotlemii  34648  ballotlemic  34651  ballotlem1c  34652  hgt750lem  34795  hgt750leme  34802  0nn0m1nnn0  35295  faclimlem1  35925  nn0prpwlem  36504  nn0prpw  36505  poimirlem32  37973  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  incsequz  38069  bfplem1  38143  rrncmslem  38153  60gcd7e1  42444  12lcm5e60  42447  60lcm7e420  42449  lcm1un  42452  lcmineqlem10  42477  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  aks4d1p1p7  42513  aks6d1c1p8  42554  sticksstones9  42593  sticksstones11  42595  aks6d1c7lem1  42619  3cubes  43122  jm2.23  43424  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  relexp2  44104  iunrelexpmin1  44135  iunrelexpmin2  44139  dftrcl3  44147  fvtrcllb1d  44149  cotrcltrcl  44152  corcltrcl  44166  cotrclrcl  44169  prmunb2  44738  sumsnd  45457  nnn0  45807  xrralrecnnge  45819  iooiinicc  45972  iooiinioc  45986  mccl  46028  sumnnodd  46060  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem8  46509  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  fourierdlem31  46566  nnfoctbdjlem  46883  hoicvrrex  46984  hoidmvlelem3  47025  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  ovnsubadd2lem  47073  iinhoiicclem  47101  vonicclem2  47112  nthrucw  47316  1elfzo1ceilhalf1  47789  iccpartlt  47884  257prm  48024  fmtnoprmfac2lem1  48029  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  fmtno5nprm  48046  3ndvds4  48058  139prmALT  48059  31prm  48060  127prm  48062  3exp4mod41  48079  41prothprmlem2  48081  perfectALTVlem1  48197  perfectALTVlem2  48198  2exp340mod341  48209  341fppr2  48210  4fppr1  48211  nnsum3primesprm  48266  bgoldbtbndlem1  48281  tgblthelfgott  48291  nnsgrpmgm  48652  nnsgrpnmnd  48654  blennn0elnn  49053  blen1  49060  ackval42  49172