Theorem 1nn 9196

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 9187	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2298	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8221	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3941	. . . 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 2806	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2295	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2295	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2743	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2951	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2591	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2202  {cab 2217  ∀wral 2511  ∩ cint 3933  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078  ℕcn 9185

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8169

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-int 3934  df-inn 9186

This theorem is referenced by:  nnind  9201  nn1suc  9204  2nn  9347  1nn0  9460  nn0p1nn  9483  1z  9549  neg1z  9555  elz2  9595  nneoor  9626  9p1e10  9657  indstr  9871  elnn1uz2  9885  zq  9904  qreccl  9920  fz01or  10391  exp3vallem  10848  exp1  10853  nnexpcl  10860  expnbnd  10971  3dec  11022  fac1  11037  faccl  11043  faclbnd3  11051  fiubnn  11140  lsw0  11210  cats1un  11351  cats1fvn  11394  cats1fvnd  11395  resqrexlemf1  11631  resqrexlemcalc3  11639  resqrexlemnmsq  11640  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemglsq  11645  resqrexlemga  11646  sumsnf  12033  cvgratnnlemnexp  12148  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  prodsnf  12216  fprodnncl  12234  eftlub  12314  eirraplem  12401  n2dvds1  12536  ndvdsp1  12556  5ndvds6  12559  gcd1  12621  bezoutr1  12667  ncoprmgcdne1b  12724  1nprm  12749  1idssfct  12750  isprm2lem  12751  qden1elz  12840  phicl2  12849  phi1  12854  phiprm  12858  eulerthlema  12865  pcpre1  12928  pczpre  12933  pcmptcl  12978  pcmpt  12979  infpnlem2  12996  mul4sq  13030  exmidunben  13110  nninfdc  13137  base0  13195  baseval  13198  baseid  13199  basendx  13200  basendxnn  13201  1strstrg  13262  2strstrg  13265  basendxnplusgndx  13271  basendxnmulrndx  13280  rngstrg  13281  lmodstrd  13310  topgrpstrd  13342  ocndx  13357  ocid  13358  basendxnocndx  13359  plendxnocndx  13360  basendxltdsndx  13365  dsndxnplusgndx  13367  dsndxnmulrndx  13368  slotsdnscsi  13369  dsndxntsetndx  13370  slotsdifdsndx  13371  basendxltunifndx  13375  unifndxntsetndx  13377  slotsdifunifndx  13378  mulg1  13779  mulg2  13781  mulgnndir  13801  setsmsdsg  15274  perfectlem1  15796  perfectlem2  15797  lgsdir2lem1  15830  lgsdir2lem4  15833  lgsdir2lem5  15834  lgsdir  15837  lgsne0  15840  lgs1  15846  lgsquad2lem2  15884  basendxltedgfndx  15934  clwwlkn1  16342  konigsberglem1  16412  trilpolemgt1  16754