Theorem peano2nn 7667

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	⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)

Proof of Theorem peano2nn

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 7657	. . . . . 6 ⊢ ℕ = ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}
2	1	eleq2i 2101	. . . . 5 ⊢ (A ∈ ℕ ↔ A ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)})
3		elintg 3614	. . . . 5 ⊢ (A ∈ ℕ → (A ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔ ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z))
4	2, 3	syl5bb 181	. . . 4 ⊢ (A ∈ ℕ → (A ∈ ℕ ↔ ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z))
5	4	ibi 165	. . 3 ⊢ (A ∈ ℕ → ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z)
6		vex 2554	. . . . . . . 8 ⊢ z ∈ V
7		eleq2 2098	. . . . . . . . 9 ⊢ (x = z → (1 ∈ x ↔ 1 ∈ z))
8		eleq2 2098	. . . . . . . . . 10 ⊢ (x = z → ((y + 1) ∈ x ↔ (y + 1) ∈ z))
9	8	raleqbi1dv 2507	. . . . . . . . 9 ⊢ (x = z → (∀y ∈ x (y + 1) ∈ x ↔ ∀y ∈ z (y + 1) ∈ z))
10	7, 9	anbi12d 442	. . . . . . . 8 ⊢ (x = z → ((1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x) ↔ (1 ∈ z ∧ ∀y ∈ z (y + 1) ∈ z)))
11	6, 10	elab 2681	. . . . . . 7 ⊢ (z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔ (1 ∈ z ∧ ∀y ∈ z (y + 1) ∈ z))
12	11	simprbi 260	. . . . . 6 ⊢ (z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} → ∀y ∈ z (y + 1) ∈ z)
13		oveq1 5462	. . . . . . . 8 ⊢ (y = A → (y + 1) = (A + 1))
14	13	eleq1d 2103	. . . . . . 7 ⊢ (y = A → ((y + 1) ∈ z ↔ (A + 1) ∈ z))
15	14	rspcva 2648	. . . . . 6 ⊢ ((A ∈ z ∧ ∀y ∈ z (y + 1) ∈ z) → (A + 1) ∈ z)
16	12, 15	sylan2 270	. . . . 5 ⊢ ((A ∈ z ∧ z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}) → (A + 1) ∈ z)
17	16	expcom 109	. . . 4 ⊢ (z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} → (A ∈ z → (A + 1) ∈ z))
18	17	ralimia 2376	. . 3 ⊢ (∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z → ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z)
19	5, 18	syl 14	. 2 ⊢ (A ∈ ℕ → ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z)
20		nnre 7662	. . . 4 ⊢ (A ∈ ℕ → A ∈ ℝ)
21		1red 6800	. . . 4 ⊢ (A ∈ ℕ → 1 ∈ ℝ)
22	20, 21	readdcld 6812	. . 3 ⊢ (A ∈ ℕ → (A + 1) ∈ ℝ)
23	1	eleq2i 2101	. . . 4 ⊢ ((A + 1) ∈ ℕ ↔ (A + 1) ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)})
24		elintg 3614	. . . 4 ⊢ ((A + 1) ∈ ℝ → ((A + 1) ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔ ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z))
25	23, 24	syl5bb 181	. . 3 ⊢ ((A + 1) ∈ ℝ → ((A + 1) ∈ ℕ ↔ ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z))
26	22, 25	syl 14	. 2 ⊢ (A ∈ ℕ → ((A + 1) ∈ ℕ ↔ ∀z ∈ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z))
27	19, 26	mpbird 156	1 ⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∩ cint 3606  (class class class)co 5455  ℝcr 6670  1c1 6672   + caddc 6674  ℕcn 7655

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-cnex 6734  ax-resscn 6735  ax-1re 6737  ax-addrcl 6740

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458  df-inn 7656

This theorem is referenced by:  peano2nnd  7670  nnind  7671  nnaddcl  7675  2nn  7815  3nn  7816  4nn  7817  5nn  7818  6nn  7819  7nn  7820  8nn  7821  9nn  7822  10nn  7823  nneoor  8076  fzonn0p1p1  8799  expp1  8876