Theorem 1nn 9144

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 9135	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2296	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8168	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3934	. . . 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 2803	. . . 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 2948	. . 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 3926  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  ℕcn 9133

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 8116

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 2802  df-int 3927  df-inn 9134

This theorem is referenced by:  nnind  9149  nn1suc  9152  2nn  9295  1nn0  9408  nn0p1nn  9431  1z  9495  neg1z  9501  elz2  9541  nneoor  9572  9p1e10  9603  indstr  9817  elnn1uz2  9831  zq  9850  qreccl  9866  fz01or  10336  exp3vallem  10792  exp1  10797  nnexpcl  10804  expnbnd  10915  3dec  10966  fac1  10981  faccl  10987  faclbnd3  10995  fiubnn  11084  lsw0  11151  cats1un  11292  cats1fvn  11335  cats1fvnd  11336  resqrexlemf1  11559  resqrexlemcalc3  11567  resqrexlemnmsq  11568  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  sumsnf  11960  cvgratnnlemnexp  12075  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  prodsnf  12143  fprodnncl  12161  eftlub  12241  eirraplem  12328  n2dvds1  12463  ndvdsp1  12483  5ndvds6  12486  gcd1  12548  bezoutr1  12594  ncoprmgcdne1b  12651  1nprm  12676  1idssfct  12677  isprm2lem  12678  qden1elz  12767  phicl2  12776  phi1  12781  phiprm  12785  eulerthlema  12792  pcpre1  12855  pczpre  12860  pcmptcl  12905  pcmpt  12906  infpnlem2  12923  mul4sq  12957  exmidunben  13037  nninfdc  13064  base0  13122  baseval  13125  baseid  13126  basendx  13127  basendxnn  13128  1strstrg  13189  2strstrg  13192  basendxnplusgndx  13198  basendxnmulrndx  13207  rngstrg  13208  lmodstrd  13237  topgrpstrd  13269  ocndx  13284  ocid  13285  basendxnocndx  13286  plendxnocndx  13287  basendxltdsndx  13292  dsndxnplusgndx  13294  dsndxnmulrndx  13295  slotsdnscsi  13296  dsndxntsetndx  13297  slotsdifdsndx  13298  basendxltunifndx  13302  unifndxntsetndx  13304  slotsdifunifndx  13305  mulg1  13706  mulg2  13708  mulgnndir  13728  setsmsdsg  15194  perfectlem1  15713  perfectlem2  15714  lgsdir2lem1  15747  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsdir  15754  lgsne0  15757  lgs1  15763  lgsquad2lem2  15801  basendxltedgfndx  15851  clwwlkn1  16213  trilpolemgt1  16579