Theorem 1nn 9294

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 9285	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2305	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8315	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3973	. . . 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 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  {cab 2224  ∀wral 2528  ∩ cint 3965  (class class class)co 6075  ℝcr 8168  1c1 8170   + caddc 8172  ℕcn 9283

This theorem was proved from 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 8263

This theorem 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 3966  df-inn 9284

This theorem is referenced by:  nnind  9299  nn1suc  9302  2nn  9445  1nn0  9558  nn0p1nn  9581  1z  9649  neg1z  9655  elz2  9695  nneoor  9727  9p1e10  9758  indstr  9972  elnn1uz2  9986  zq  10005  qreccl  10021  fz01or  10496  exp3vallem  10955  exp1  10960  nnexpcl  10967  expnbnd  11079  3dec  11130  fac1  11145  faccl  11151  faclbnd3  11159  fiubnn  11251  lsw0  11330  cats1un  11471  cats1fvn  11514  cats1fvnd  11515  resqrexlemf1  11752  resqrexlemcalc3  11760  resqrexlemnmsq  11761  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemglsq  11766  resqrexlemga  11767  sumsnf  12154  cvgratnnlemnexp  12269  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  prodsnf  12337  fprodnncl  12355  eftlub  12435  eirraplem  12522  n2dvds1  12657  ndvdsp1  12677  5ndvds6  12680  gcd1  12742  bezoutr1  12788  ncoprmgcdne1b  12845  1nprm  12870  1idssfct  12871  isprm2lem  12872  qden1elz  12961  phicl2  12970  phi1  12975  phiprm  12979  eulerthlema  12986  pcpre1  13049  pczpre  13054  pcmptcl  13099  pcmpt  13100  infpnlem2  13117  mul4sq  13151  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  exmidunben  13295  nninfdc  13322  base0  13380  baseval  13383  baseid  13384  basendx  13385  basendxnn  13386  1strstrg  13447  2strstrg  13450  basendxnplusgndx  13456  basendxnmulrndx  13465  rngstrg  13466  lmodstrd  13495  topgrpstrd  13527  ocndx  13542  ocid  13543  basendxnocndx  13544  plendxnocndx  13545  basendxltdsndx  13550  dsndxnplusgndx  13552  dsndxnmulrndx  13553  slotsdnscsi  13554  dsndxntsetndx  13555  slotsdifdsndx  13556  basendxltunifndx  13560  unifndxntsetndx  13562  slotsdifunifndx  13563  mulg1  13909  mulg2  13911  mulgnndir  13931  setsmsdsg  15504  logfac  15918  perfectlem1  16027  perfectlem2  16028  lgsdir2lem1  16061  lgsdir2lem4  16064  lgsdir2lem5  16065  lgsdir  16068  lgsne0  16071  lgs1  16077  lgsquad2lem2  16115  basendxltedgfndx  16165  clwwlkn1  16573  konigsberglem1  16643  trilpolemgt1  16993