Theorem 1nn 9062

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 9053	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2273	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8086	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3898	. . . 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 2776	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2270	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2270	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2715	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2921	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2565	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2177  {cab 2192  ∀wral 2485  ∩ cint 3890  (class class class)co 5956  ℝcr 7939  1c1 7941   + caddc 7943  ℕcn 9051

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1re 8034

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-int 3891  df-inn 9052

This theorem is referenced by:  nnind  9067  nn1suc  9070  2nn  9213  1nn0  9326  nn0p1nn  9349  1z  9413  neg1z  9419  elz2  9459  nneoor  9490  9p1e10  9521  indstr  9729  elnn1uz2  9743  zq  9762  qreccl  9778  fz01or  10248  exp3vallem  10702  exp1  10707  nnexpcl  10714  expnbnd  10825  3dec  10876  fac1  10891  faccl  10897  faclbnd3  10905  fiubnn  10992  lsw0  11058  cats1un  11192  resqrexlemf1  11389  resqrexlemcalc3  11397  resqrexlemnmsq  11398  resqrexlemnm  11399  resqrexlemcvg  11400  resqrexlemglsq  11403  resqrexlemga  11404  sumsnf  11790  cvgratnnlemnexp  11905  cvgratnnlemfm  11910  cvgratnnlemrate  11911  cvgratnn  11912  prodsnf  11973  fprodnncl  11991  eftlub  12071  eirraplem  12158  n2dvds1  12293  ndvdsp1  12313  5ndvds6  12316  gcd1  12378  bezoutr1  12424  ncoprmgcdne1b  12481  1nprm  12506  1idssfct  12507  isprm2lem  12508  qden1elz  12597  phicl2  12606  phi1  12611  phiprm  12615  eulerthlema  12622  pcpre1  12685  pczpre  12690  pcmptcl  12735  pcmpt  12736  infpnlem2  12753  mul4sq  12787  exmidunben  12867  nninfdc  12894  base0  12952  baseval  12955  baseid  12956  basendx  12957  basendxnn  12958  1strstrg  13018  2strstrg  13021  basendxnplusgndx  13027  basendxnmulrndx  13036  rngstrg  13037  lmodstrd  13066  topgrpstrd  13098  ocndx  13113  ocid  13114  basendxnocndx  13115  plendxnocndx  13116  basendxltdsndx  13121  dsndxnplusgndx  13123  dsndxnmulrndx  13124  slotsdnscsi  13125  dsndxntsetndx  13126  slotsdifdsndx  13127  basendxltunifndx  13131  unifndxntsetndx  13133  slotsdifunifndx  13134  mulg1  13535  mulg2  13537  mulgnndir  13557  setsmsdsg  15022  perfectlem1  15541  perfectlem2  15542  lgsdir2lem1  15575  lgsdir2lem4  15578  lgsdir2lem5  15579  lgsdir  15582  lgsne0  15585  lgs1  15591  lgsquad2lem2  15629  basendxltedgfndx  15679  trilpolemgt1  16113