Theorem 1nn 9117

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 9108	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2296	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8141	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3930	. . . 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 3922  (class class class)co 6000  ℝcr 7994  1c1 7996   + caddc 7998  ℕcn 9106

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 8089

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 3923  df-inn 9107

This theorem is referenced by:  nnind  9122  nn1suc  9125  2nn  9268  1nn0  9381  nn0p1nn  9404  1z  9468  neg1z  9474  elz2  9514  nneoor  9545  9p1e10  9576  indstr  9784  elnn1uz2  9798  zq  9817  qreccl  9833  fz01or  10303  exp3vallem  10757  exp1  10762  nnexpcl  10769  expnbnd  10880  3dec  10931  fac1  10946  faccl  10952  faclbnd3  10960  fiubnn  11047  lsw0  11114  cats1un  11248  cats1fvn  11291  cats1fvnd  11292  resqrexlemf1  11514  resqrexlemcalc3  11522  resqrexlemnmsq  11523  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemglsq  11528  resqrexlemga  11529  sumsnf  11915  cvgratnnlemnexp  12030  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  prodsnf  12098  fprodnncl  12116  eftlub  12196  eirraplem  12283  n2dvds1  12418  ndvdsp1  12438  5ndvds6  12441  gcd1  12503  bezoutr1  12549  ncoprmgcdne1b  12606  1nprm  12631  1idssfct  12632  isprm2lem  12633  qden1elz  12722  phicl2  12731  phi1  12736  phiprm  12740  eulerthlema  12747  pcpre1  12810  pczpre  12815  pcmptcl  12860  pcmpt  12861  infpnlem2  12878  mul4sq  12912  exmidunben  12992  nninfdc  13019  base0  13077  baseval  13080  baseid  13081  basendx  13082  basendxnn  13083  1strstrg  13144  2strstrg  13147  basendxnplusgndx  13153  basendxnmulrndx  13162  rngstrg  13163  lmodstrd  13192  topgrpstrd  13224  ocndx  13239  ocid  13240  basendxnocndx  13241  plendxnocndx  13242  basendxltdsndx  13247  dsndxnplusgndx  13249  dsndxnmulrndx  13250  slotsdnscsi  13251  dsndxntsetndx  13252  slotsdifdsndx  13253  basendxltunifndx  13257  unifndxntsetndx  13259  slotsdifunifndx  13260  mulg1  13661  mulg2  13663  mulgnndir  13683  setsmsdsg  15148  perfectlem1  15667  perfectlem2  15668  lgsdir2lem1  15701  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsdir  15708  lgsne0  15711  lgs1  15717  lgsquad2lem2  15755  basendxltedgfndx  15805  trilpolemgt1  16366