Theorem 1nn 9154

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 9145	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2298	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8178	. . . 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 6018  ℝcr 8031  1c1 8033   + caddc 8035  ℕcn 9143

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 8126

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 9144

This theorem is referenced by:  nnind  9159  nn1suc  9162  2nn  9305  1nn0  9418  nn0p1nn  9441  1z  9505  neg1z  9511  elz2  9551  nneoor  9582  9p1e10  9613  indstr  9827  elnn1uz2  9841  zq  9860  qreccl  9876  fz01or  10346  exp3vallem  10803  exp1  10808  nnexpcl  10815  expnbnd  10926  3dec  10977  fac1  10992  faccl  10998  faclbnd3  11006  fiubnn  11095  lsw0  11165  cats1un  11306  cats1fvn  11349  cats1fvnd  11350  resqrexlemf1  11586  resqrexlemcalc3  11594  resqrexlemnmsq  11595  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemglsq  11600  resqrexlemga  11601  sumsnf  11988  cvgratnnlemnexp  12103  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  prodsnf  12171  fprodnncl  12189  eftlub  12269  eirraplem  12356  n2dvds1  12491  ndvdsp1  12511  5ndvds6  12514  gcd1  12576  bezoutr1  12622  ncoprmgcdne1b  12679  1nprm  12704  1idssfct  12705  isprm2lem  12706  qden1elz  12795  phicl2  12804  phi1  12809  phiprm  12813  eulerthlema  12820  pcpre1  12883  pczpre  12888  pcmptcl  12933  pcmpt  12934  infpnlem2  12951  mul4sq  12985  exmidunben  13065  nninfdc  13092  base0  13150  baseval  13153  baseid  13154  basendx  13155  basendxnn  13156  1strstrg  13217  2strstrg  13220  basendxnplusgndx  13226  basendxnmulrndx  13235  rngstrg  13236  lmodstrd  13265  topgrpstrd  13297  ocndx  13312  ocid  13313  basendxnocndx  13314  plendxnocndx  13315  basendxltdsndx  13320  dsndxnplusgndx  13322  dsndxnmulrndx  13323  slotsdnscsi  13324  dsndxntsetndx  13325  slotsdifdsndx  13326  basendxltunifndx  13330  unifndxntsetndx  13332  slotsdifunifndx  13333  mulg1  13734  mulg2  13736  mulgnndir  13756  setsmsdsg  15223  perfectlem1  15742  perfectlem2  15743  lgsdir2lem1  15776  lgsdir2lem4  15779  lgsdir2lem5  15780  lgsdir  15783  lgsne0  15786  lgs1  15792  lgsquad2lem2  15830  basendxltedgfndx  15880  clwwlkn1  16288  konigsberglem1  16358  trilpolemgt1  16694