Metamath Proof Explorer

Theorem peano5nni

Description: Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of Apostol p. 34. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano5nni ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → ℕ ⊆ A

Proof

Step Hyp Ref Expression
1 df-nn ⊢ ℕ = rec ⁡ n ∈ V ⟼ n + 1 1 ω
2 df-ima ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ω = ran ⁡ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
3 1 2 eqtri ⊢ ℕ = ran ⁡ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
4 frfnom ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω Fn ω
5 4 a1i ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω Fn ω
6 fveq2 ⊢ y = ∅ → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ ∅
7 6 eleq1d ⊢ y = ∅ → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ ∅ ∈ A
8 fveq2 ⊢ y = z → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z
9 8 eleq1d ⊢ y = z → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z ∈ A
10 fveq2 ⊢ y = suc ⁡ z → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z
11 10 eleq1d ⊢ y = suc ⁡ z → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z ∈ A
12 ax-1cn ⊢ 1 ∈ ℂ
13 fr0g ⊢ 1 ∈ ℂ → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ ∅ = 1
14 12 13 ax-mp ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ ∅ = 1
15 simpl ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → 1 ∈ A
16 14 15 eqeltrid ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ ∅ ∈ A
17 oveq1 ⊢ x = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z → x + 1 = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1
18 17 eleq1d ⊢ x = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z → x + 1 ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ A
19 18 rspccv ⊢ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ A
20 19 ad2antlr ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A ∧ z ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ A
21 ovex ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ V
22 eqid ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
23 oveq1 ⊢ y = n → y + 1 = n + 1
24 oveq1 ⊢ y = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z → y + 1 = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1
25 22 23 24 frsucmpt2 ⊢ z ∈ ω ∧ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ V → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1
26 21 25 mpan2 ⊢ z ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1
27 26 eleq1d ⊢ z ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ A
28 27 adantl ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A ∧ z ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z ∈ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z + 1 ∈ A
29 20 28 sylibrd ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A ∧ z ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z ∈ A
30 29 expcom ⊢ z ∈ ω → 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ z ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ suc ⁡ z ∈ A
31 7 9 11 16 30 finds2 ⊢ y ∈ ω → 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A
32 31 com12 ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → y ∈ ω → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A
33 32 ralrimiv ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → ∀ y ∈ ω rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A
34 ffnfv ⊢ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω : ω ⟶ A ↔ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω Fn ω ∧ ∀ y ∈ ω rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⁡ y ∈ A
35 5 33 34 sylanbrc ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω : ω ⟶ A
36 35 frnd ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → ran ⁡ rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω ⊆ A
37 3 36 eqsstrid ⊢ 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → ℕ ⊆ A