Theorem 1nn 9298

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)

Assertion

Ref	Expression
1nn	⊢ 1 ∈ ℕ

Proof of Theorem 1nn

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 9289	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2305	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8319	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3976	. . . 4 ⊢ (1 ∈ ℝ → (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
5	3, 4	ax-mp 5	. . 3 ⊢ (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
6	2, 5	bitri 184	. 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7		vex 2824	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2302	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2302	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2761	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 477	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2970	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2608	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  {cab 2224  ∀wral 2528  ∩ cint 3968  (class class class)co 6079  ℝcr 8172  1c1 8174   + caddc 8176  ℕcn 9287

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8267

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-int 3969  df-inn 9288

This theorem is used by:  nnind  9303  nn1suc  9306  2nn  9449  1nn0  9562  nn0p1nn  9585  1z  9653  neg1z  9659  elz2  9699  nneoor  9731  9p1e10  9762  indstr  9976  elnn1uz2  9990  zq  10009  qreccl  10025  fz01or  10501  exp3vallem  10960  exp1  10965  nnexpcl  10972  expnbnd  11084  3dec  11135  fac1  11150  faccl  11156  faclbnd3  11164  fiubnn  11256  lsw0  11335  cats1un  11476  cats1fvn  11519  cats1fvnd  11520  resqrexlemf1  11757  resqrexlemcalc3  11765  resqrexlemnmsq  11766  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemglsq  11771  resqrexlemga  11772  sumsnf  12159  cvgratnnlemnexp  12274  cvgratnnlemfm  12279  cvgratnnlemrate  12280  cvgratnn  12281  prodsnf  12342  fprodnncl  12360  eftlub  12440  eirraplem  12527  n2dvds1  12662  ndvdsp1  12682  5ndvds6  12685  gcd1  12747  bezoutr1  12793  ncoprmgcdne1b  12850  1nprm  12875  1idssfct  12876  isprm2lem  12877  qden1elz  12966  phicl2  12975  phi1  12980  phiprm  12984  eulerthlema  12991  pcpre1  13054  pczpre  13059  pcmptcl  13104  pcmpt  13105  infpnlem2  13122  mul4sq  13156  ballotfilem4  13224  ballotfilemi1  13228  ballotfilemii  13229  ballotfilemic  13233  ballotfilem1c  13234  exmidunben  13300  nninfdc  13327  base0  13385  baseval  13388  baseid  13389  basendx  13390  basendxnn  13391  1strstrg  13453  2strstrg  13456  basendxnplusgndx  13462  basendxnmulrndx  13471  rngstrg  13472  lmodstrd  13501  topgrpstrd  13533  ocndx  13548  ocid  13549  basendxnocndx  13550  plendxnocndx  13551  basendxltdsndx  13556  dsndxnplusgndx  13558  dsndxnmulrndx  13559  slotsdnscsi  13560  dsndxntsetndx  13561  slotsdifdsndx  13562  basendxltunifndx  13566  unifndxntsetndx  13568  slotsdifunifndx  13569  mulg1  13915  mulg2  13917  mulgnndir  13937  setsmsdsg  15564  logfac  15978  log2ublog2  16069  perfectlem1  16096  perfectlem2  16097  lgsdir2lem1  16130  lgsdir2lem4  16133  lgsdir2lem5  16134  lgsdir  16137  lgsne0  16140  lgs1  16146  lgsquad2lem2  16184  basendxltedgfndx  16234  clwwlkn1  16642  konigsberglem1  16712  trilpolemgt1  17063