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 ⊢Ⅎ_yx∈ℕ|φ
22 nfcv ⊢Ⅎ_wx∈ℕ|φ
23 nfv ⊢Ⅎwy+1∈x∈ℕ|φ
24 21 nfel2 ⊢Ⅎyw+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∈ℕ→τ