Theorem 1nn 9153

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 9144	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2298	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8177	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3936	. . . 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 2805	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2295	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2295	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2742	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2950	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2590	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2202  {cab 2217  ∀wral 2510  ∩ cint 3928  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034  ℕcn 9142

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-int 3929  df-inn 9143

This theorem is referenced by:  nnind  9158  nn1suc  9161  2nn  9304  1nn0  9417  nn0p1nn  9440  1z  9504  neg1z  9510  elz2  9550  nneoor  9581  9p1e10  9612  indstr  9826  elnn1uz2  9840  zq  9859  qreccl  9875  fz01or  10345  exp3vallem  10801  exp1  10806  nnexpcl  10813  expnbnd  10924  3dec  10975  fac1  10990  faccl  10996  faclbnd3  11004  fiubnn  11093  lsw0  11160  cats1un  11301  cats1fvn  11344  cats1fvnd  11345  resqrexlemf1  11568  resqrexlemcalc3  11576  resqrexlemnmsq  11577  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemglsq  11582  resqrexlemga  11583  sumsnf  11969  cvgratnnlemnexp  12084  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  prodsnf  12152  fprodnncl  12170  eftlub  12250  eirraplem  12337  n2dvds1  12472  ndvdsp1  12492  5ndvds6  12495  gcd1  12557  bezoutr1  12603  ncoprmgcdne1b  12660  1nprm  12685  1idssfct  12686  isprm2lem  12687  qden1elz  12776  phicl2  12785  phi1  12790  phiprm  12794  eulerthlema  12801  pcpre1  12864  pczpre  12869  pcmptcl  12914  pcmpt  12915  infpnlem2  12932  mul4sq  12966  exmidunben  13046  nninfdc  13073  base0  13131  baseval  13134  baseid  13135  basendx  13136  basendxnn  13137  1strstrg  13198  2strstrg  13201  basendxnplusgndx  13207  basendxnmulrndx  13216  rngstrg  13217  lmodstrd  13246  topgrpstrd  13278  ocndx  13293  ocid  13294  basendxnocndx  13295  plendxnocndx  13296  basendxltdsndx  13301  dsndxnplusgndx  13303  dsndxnmulrndx  13304  slotsdnscsi  13305  dsndxntsetndx  13306  slotsdifdsndx  13307  basendxltunifndx  13311  unifndxntsetndx  13313  slotsdifunifndx  13314  mulg1  13715  mulg2  13717  mulgnndir  13737  setsmsdsg  15203  perfectlem1  15722  perfectlem2  15723  lgsdir2lem1  15756  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsdir  15763  lgsne0  15766  lgs1  15772  lgsquad2lem2  15810  basendxltedgfndx  15860  clwwlkn1  16268  trilpolemgt1  16643