Theorem 1nn 9137

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 9128	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2296	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8161	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3931	. . . 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 2802	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2293	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2293	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2740	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2947	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2588	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∩ cint 3923  (class class class)co 6010  ℝcr 8014  1c1 8016   + caddc 8018  ℕcn 9126

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8109

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-int 3924  df-inn 9127

This theorem is referenced by:  nnind  9142  nn1suc  9145  2nn  9288  1nn0  9401  nn0p1nn  9424  1z  9488  neg1z  9494  elz2  9534  nneoor  9565  9p1e10  9596  indstr  9805  elnn1uz2  9819  zq  9838  qreccl  9854  fz01or  10324  exp3vallem  10779  exp1  10784  nnexpcl  10791  expnbnd  10902  3dec  10953  fac1  10968  faccl  10974  faclbnd3  10982  fiubnn  11070  lsw0  11137  cats1un  11274  cats1fvn  11317  cats1fvnd  11318  resqrexlemf1  11540  resqrexlemcalc3  11548  resqrexlemnmsq  11549  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemglsq  11554  resqrexlemga  11555  sumsnf  11941  cvgratnnlemnexp  12056  cvgratnnlemfm  12061  cvgratnnlemrate  12062  cvgratnn  12063  prodsnf  12124  fprodnncl  12142  eftlub  12222  eirraplem  12309  n2dvds1  12444  ndvdsp1  12464  5ndvds6  12467  gcd1  12529  bezoutr1  12575  ncoprmgcdne1b  12632  1nprm  12657  1idssfct  12658  isprm2lem  12659  qden1elz  12748  phicl2  12757  phi1  12762  phiprm  12766  eulerthlema  12773  pcpre1  12836  pczpre  12841  pcmptcl  12886  pcmpt  12887  infpnlem2  12904  mul4sq  12938  exmidunben  13018  nninfdc  13045  base0  13103  baseval  13106  baseid  13107  basendx  13108  basendxnn  13109  1strstrg  13170  2strstrg  13173  basendxnplusgndx  13179  basendxnmulrndx  13188  rngstrg  13189  lmodstrd  13218  topgrpstrd  13250  ocndx  13265  ocid  13266  basendxnocndx  13267  plendxnocndx  13268  basendxltdsndx  13273  dsndxnplusgndx  13275  dsndxnmulrndx  13276  slotsdnscsi  13277  dsndxntsetndx  13278  slotsdifdsndx  13279  basendxltunifndx  13283  unifndxntsetndx  13285  slotsdifunifndx  13286  mulg1  13687  mulg2  13689  mulgnndir  13709  setsmsdsg  15175  perfectlem1  15694  perfectlem2  15695  lgsdir2lem1  15728  lgsdir2lem4  15731  lgsdir2lem5  15732  lgsdir  15735  lgsne0  15738  lgs1  15744  lgsquad2lem2  15782  basendxltedgfndx  15832  clwwlkn1  16186  trilpolemgt1  16521