Theorem 1nn 12215

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 11170	. . . 4 ⊢ 1 ∈ V
2		fr0g 8401	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8400	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7864	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7056	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 702	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2858	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12205	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5656	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2784	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2860	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ∅c0 4283   ↦ cmpt 5178  ran crn 5644   ↾ cres 5645   “ cima 5646   Fn wfn 6511  ‘cfv 6516  (class class class)co 7391  ωcom 7841  reccrdg 8374  1c1 11068   + caddc 11070  ℕcn 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205

This theorem is referenced by:  dfnn2  12217  dfnn3  12218  nnind  12222  nn1suc  12226  nnmulcom  12265  2nn  12285  nnunb  12471  1nn0  12491  nn0p1nn  12514  elz2  12580  1z  12595  neg1z  12601  nneo  12651  9p1e10  12684  11nn  12707  elnn1uz2  12920  zq  12949  rpnnen1lem4  12975  rpnnen1lem5  12976  1elfzo1  13714  ser1const  14065  exp1  14074  nnexpcl  14081  expnbnd  14239  fac1  14284  faccl  14290  faclbnd3  14299  faclbnd4lem1  14300  faclbnd4lem2  14301  faclbnd4lem3  14302  faclbnd4lem4  14303  lsw0  14572  ccat2s1p1  14637  cats1un  14728  revs1  14772  cats1fvn  14865  relexpsucnnl  15037  relexpaddg  15060  isercolllem2  15684  isercolllem3  15685  isercoll  15686  sumsnf  15761  climcndslem1  15870  climcndslem2  15871  fprodnncl  15976  prodsn  15983  prodsnf  15985  nnrisefaccl  16040  eftlub  16132  eirrlem  16227  rpnnen2lem5  16241  rpnnen2lem8  16244  rpnnen2lem12  16248  dvdsle  16335  ndvdsp1  16436  5ndvds6  16439  gcd1  16553  bezoutr1  16594  1nprm  16704  1idssfct  16705  isprm2lem  16706  qden1elz  16783  phi1  16799  phiprm  16803  pcpre1  16869  pczpre  16874  pcmptcl  16918  pcmpt  16919  infpnlem2  16938  prmreclem1  16943  prmreclem6  16948  mul4sq  16981  vdwmc2  17006  vdwlem8  17015  vdwlem13  17020  vdwnnlem3  17024  prmocl  17061  prmop1  17065  fvprmselelfz  17071  fvprmselgcd1  17072  prmolefac  17073  prmodvdslcmf  17074  prmgapprmo  17089  5prm  17135  7prm  17137  10nprm  17140  11prm  17142  13prm  17143  17prm  17144  19prm  17145  37prm  17148  43prm  17149  83prm  17150  139prm  17151  163prm  17152  317prm  17153  631prm  17154  1259lem4  17161  1259lem5  17162  1259prm  17163  2503lem3  17166  2503prm  17167  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  4001prm  17172  baseid  17239  basendx  17245  basendxnn  17246  rngstr  17318  lmodstr  17345  topgrpstr  17381  otpsstr  17396  ocndx  17401  ocid  17402  basendxnocndx  17403  plendxnocndx  17404  basendxltdsndx  17408  dsndxnplusgndx  17410  dsndxnmulrndx  17411  slotsdnscsi  17412  dsndxntsetndx  17413  slotsdifdsndx  17414  basendxltunifndx  17418  unifndxntsetndx  17420  slotsdifunifndx  17421  slotsbhcdif  17435  slotsdifocndx  17437  catstr  17984  ipostr  18552  mulgfval  19102  mulg1  19114  mulg2  19116  od1  19590  0subgALT  19599  gex1  19622  efgsval2  19764  efgsp1  19768  torsubg  19885  pgpfaclem1  20114  pmatcollpw3fi1lem2  22835  hauspwdom  23549  imasdsf1olem  24421  cphipval  25293  bcthlem4  25377  bcth3  25381  ovolmge0  25527  ovollb2  25539  ovolctb  25540  ovolunlem1a  25546  ovolunlem1  25547  ovoliunlem1  25552  ovoliun  25555  ovoliun2  25556  ovolicc1  25566  voliunlem1  25600  volsup  25606  ioombl1lem2  25609  ioombl1lem4  25611  uniioombllem1  25631  uniioombllem2  25633  uniioombllem6  25638  itg1climres  25764  itg2seq  25792  itg2monolem1  25800  itg2monolem2  25801  itg2monolem3  25802  itg2mono  25803  itg2i1fseq2  25806  itg2cnlem1  25811  aalioulem5  26388  aaliou2b  26393  aaliou3lem4  26398  aaliou3lem7  26401  log2ub  27002  emcllem6  27053  emcllem7  27054  lgam1  27116  gam1  27117  ftalem7  27131  efnnfsumcl  27155  vmaprm  27169  efvmacl  27172  efchtdvds  27211  vma1  27218  prmorcht  27230  sqff1o  27234  pclogsum  27267  perfectlem1  27281  perfectlem2  27282  bpos1  27335  bposlem5  27340  lgsdir  27384  lgs1  27393  lgsquad2lem2  27437  addsqn2reu  27493  addsqrexnreu  27494  dchrmusumlema  27545  dchrisum0lema  27566  slotsinbpsd  28598  slotslnbpsd  28599  trkgstr  28601  eengstr  29138  basendxltedgfndx  29152  usgrexmplef  29417  lfgrn1cycl  29962  clwwlkn1  30200  ipval2  30867  opsqrlem2  32301  ssnnssfz  32950  znumd  32976  zdend  32977  nnindf  32983  nn0min  32984  isarchi3  33328  eufndx  33438  eufid  33439  constrext2chnlem  34008  iconstr  34024  rge0scvg  34207  qqh0  34242  qqh1  34243  esumfzf  34327  esumfsup  34328  esumpcvgval  34336  voliune  34487  eulerpartgbij  34630  eulerpartlemgs2  34638  fib2  34660  rrvsum  34712  ballotlem4  34757  ballotlemi1  34761  ballotlemii  34762  ballotlemic  34765  ballotlem1c  34766  hgt750lem  34906  hgt750leme  34913  0nn0m1nnn0  35424  faclimlem1  36054  nn0prpwlem  36643  nn0prpw  36644  poimirlem32  38112  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  incsequz  38208  bfplem1  38282  rrncmslem  38292  60gcd7e1  42583  12lcm5e60  42586  60lcm7e420  42588  lcm1un  42591  lcmineqlem10  42616  3lexlogpow5ineq1  42632  3lexlogpow5ineq2  42633  aks4d1p1p7  42652  aks6d1c1p8  42693  sticksstones9  42732  sticksstones11  42734  aks6d1c7lem1  42758  3cubes  43232  jm2.23  43534  rmydioph  43552  rmxdioph  43554  expdiophlem2  43560  expdioph  43561  relexp2  44214  iunrelexpmin1  44245  iunrelexpmin2  44249  dftrcl3  44257  fvtrcllb1d  44259  cotrcltrcl  44262  corcltrcl  44276  cotrclrcl  44279  prmunb2  44848  sumsnd  45567  nnn0  45914  xrralrecnnge  45926  iooiinicc  46079  iooiinioc  46093  mccl  46135  sumnnodd  46167  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  stirlinglem8  46616  stirlinglem11  46619  stirlinglem12  46620  stirlinglem13  46621  fourierdlem31  46673  nnfoctbdjlem  46990  hoicvrrex  47091  hoidmvlelem3  47132  ovnhoilem1  47136  ovnhoilem2  47137  ovnlecvr2  47145  ovnsubadd2lem  47180  iinhoiicclem  47208  vonicclem2  47219  nthrucw  47423  1elfzo1ceilhalf1  47896  iccpartlt  47991  257prm  48131  fmtnoprmfac2lem1  48136  fmtno4prmfac193  48143  fmtno4nprmfac193  48144  fmtno5nprm  48153  3ndvds4  48165  139prmALT  48166  31prm  48167  127prm  48169  3exp4mod41  48186  41prothprmlem2  48188  perfectALTVlem1  48304  perfectALTVlem2  48305  2exp340mod341  48316  341fppr2  48317  4fppr1  48318  nnsum3primesprm  48373  bgoldbtbndlem1  48388  tgblthelfgott  48398  nnsgrpmgm  48759  nnsgrpnmnd  48761  blennn0elnn  49160  blen1  49167  ackval42  49279