Metamath Proof Explorer

Theorem nnindf

Description: Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018)

Ref Expression
Hypotheses nnindf.x ⊢ Ⅎ y φ
nnindf.1 ⊢ x = 1 → φ ↔ ψ
nnindf.2 ⊢ x = y → φ ↔ χ
nnindf.3 ⊢ x = y + 1 → φ ↔ θ
nnindf.4 ⊢ x = A → φ ↔ τ
nnindf.5 ⊢ ψ
nnindf.6 ⊢ y ∈ ℕ → χ → θ
Assertion nnindf ⊢ A ∈ ℕ → τ

Proof

Step Hyp Ref Expression
1 nnindf.x ⊢ Ⅎ y φ
2 nnindf.1 ⊢ x = 1 → φ ↔ ψ
3 nnindf.2 ⊢ x = y → φ ↔ χ
4 nnindf.3 ⊢ x = y + 1 → φ ↔ θ
5 nnindf.4 ⊢ x = A → φ ↔ τ
6 nnindf.5 ⊢ ψ
7 nnindf.6 ⊢ y ∈ ℕ → χ → θ
8 1nn ⊢ 1 ∈ ℕ
9 2 elrab ⊢ 1 ∈ x ∈ ℕ | φ ↔ 1 ∈ ℕ ∧ ψ
10 8 6 9 mpbir2an ⊢ 1 ∈ x ∈ ℕ | φ
11 elrabi ⊢ y ∈ x ∈ ℕ | φ → y ∈ ℕ
12 peano2nn ⊢ y ∈ ℕ → y + 1 ∈ ℕ
13 12 a1d ⊢ y ∈ ℕ → y ∈ ℕ → y + 1 ∈ ℕ
14 13 7 anim12d ⊢ y ∈ ℕ → y ∈ ℕ ∧ χ → y + 1 ∈ ℕ ∧ θ
15 3 elrab ⊢ y ∈ x ∈ ℕ | φ ↔ y ∈ ℕ ∧ χ
16 4 elrab ⊢ y + 1 ∈ x ∈ ℕ | φ ↔ y + 1 ∈ ℕ ∧ θ
17 14 15 16 3imtr4g ⊢ y ∈ ℕ → y ∈ x ∈ ℕ | φ → y + 1 ∈ x ∈ ℕ | φ
18 11 17 mpcom ⊢ y ∈ x ∈ ℕ | φ → y + 1 ∈ x ∈ ℕ | φ
19 18 rgen ⊢ ∀ y ∈ x ∈ ℕ | φ y + 1 ∈ x ∈ ℕ | φ
20 nfcv ⊢ Ⅎ _ y ℕ
21 1 20 nfrabw ⊢ Ⅎ _ y x ∈ ℕ | φ
22 nfcv ⊢ Ⅎ _ w x ∈ ℕ | φ
23 nfv ⊢ Ⅎ w y + 1 ∈ x ∈ ℕ | φ
24 21 nfel2 ⊢ Ⅎ y w + 1 ∈ x ∈ ℕ | φ
25 oveq1 ⊢ y = w → y + 1 = w + 1
26 25 eleq1d ⊢ y = w → y + 1 ∈ x ∈ ℕ | φ ↔ w + 1 ∈ x ∈ ℕ | φ
27 21 22 23 24 26 cbvralfw ⊢ ∀ y ∈ x ∈ ℕ | φ y + 1 ∈ x ∈ ℕ | φ ↔ ∀ w ∈ x ∈ ℕ | φ w + 1 ∈ x ∈ ℕ | φ
28 19 27 mpbi ⊢ ∀ w ∈ x ∈ ℕ | φ w + 1 ∈ x ∈ ℕ | φ
29 peano5nni ⊢ 1 ∈ x ∈ ℕ | φ ∧ ∀ w ∈ x ∈ ℕ | φ w + 1 ∈ x ∈ ℕ | φ → ℕ ⊆ x ∈ ℕ | φ
30 10 28 29 mp2an ⊢ ℕ ⊆ x ∈ ℕ | φ
31 30 sseli ⊢ A ∈ ℕ → A ∈ x ∈ ℕ | φ
32 5 elrab ⊢ A ∈ x ∈ ℕ | φ ↔ A ∈ ℕ ∧ τ
33 31 32 sylib ⊢ A ∈ ℕ → A ∈ ℕ ∧ τ
34 33 simprd ⊢ A ∈ ℕ → τ