Theorem peano2nn 8497

Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
peano2nn	⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nn

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 8487	. . . . . 6 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2155	. . . . 5 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		elintg 3704	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧))
4	2, 3	syl5bb 191	. . . 4 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧))
5	4	ibi 175	. . 3 ⊢ (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧)
6		vex 2625	. . . . . . . 8 ⊢ 𝑧 ∈ V
7		eleq2 2152	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
8		eleq2 2152	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
9	8	raleqbi1dv 2573	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
10	7, 9	anbi12d 458	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
11	6, 10	elab 2763	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
12	11	simprbi 270	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)
13		oveq1 5675	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 + 1) = (𝐴 + 1))
14	13	eleq1d 2157	. . . . . . 7 ⊢ (𝑦 = 𝐴 → ((𝑦 + 1) ∈ 𝑧 ↔ (𝐴 + 1) ∈ 𝑧))
15	14	rspcva 2723	. . . . . 6 ⊢ ((𝐴 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → (𝐴 + 1) ∈ 𝑧)
16	12, 15	sylan2 281	. . . . 5 ⊢ ((𝐴 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) → (𝐴 + 1) ∈ 𝑧)
17	16	expcom 115	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → (𝐴 ∈ 𝑧 → (𝐴 + 1) ∈ 𝑧))
18	17	ralimia 2437	. . 3 ⊢ (∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
19	5, 18	syl 14	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
20		nnre 8492	. . . 4 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
21		1red 7566	. . . 4 ⊢ (𝐴 ∈ ℕ → 1 ∈ ℝ)
22	20, 21	readdcld 7580	. . 3 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℝ)
23	1	eleq2i 2155	. . . 4 ⊢ ((𝐴 + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
24		elintg 3704	. . . 4 ⊢ ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
25	23, 24	syl5bb 191	. . 3 ⊢ ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
26	22, 25	syl 14	. 2 ⊢ (𝐴 ∈ ℕ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
27	19, 26	mpbird 166	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1290   ∈ wcel 1439  {cab 2075  ∀wral 2360  ∩ cint 3696  (class class class)co 5668  ℝcr 7412  1c1 7414   + caddc 7416  ℕcn 8485

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-cnex 7499  ax-resscn 7500  ax-1re 7502  ax-addrcl 7505

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2624  df-un 3006  df-in 3008  df-ss 3015  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-br 3854  df-iota 4995  df-fv 5038  df-ov 5671  df-inn 8486

This theorem is referenced by:  peano2nnd  8500  nnind  8501  nnaddcl  8505  2nn  8640  3nn  8641  4nn  8642  5nn  8643  6nn  8644  7nn  8645  8nn  8646  9nn  8647  nneoor  8911  10nn  8955  nnsplit  9611  fzonn0p1p1  9687  expp1  10025  facp1  10201  resqrexlemfp1  10505  resqrexlemcalc3  10512  trireciplem  10957  trirecip  10958  cvgratnnlemnexp  10981  cvgratz  10989  nno  11247  nnoddm1d2  11251  rplpwr  11357  prmind2  11443  sqrt2irr  11482