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 𝑦 𝜑
nnindf.1 ( 𝑥 = 1 → ( 𝜑𝜓 ) )
nnindf.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
nnindf.3 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑𝜃 ) )
nnindf.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
nnindf.5 𝜓
nnindf.6 ( 𝑦 ∈ ℕ → ( 𝜒𝜃 ) )
Assertion nnindf ( 𝐴 ∈ ℕ → 𝜏 )

Proof

Step Hyp Ref Expression
1 nnindf.x 𝑦 𝜑
2 nnindf.1 ( 𝑥 = 1 → ( 𝜑𝜓 ) )
3 nnindf.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
4 nnindf.3 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑𝜃 ) )
5 nnindf.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
6 nnindf.5 𝜓
7 nnindf.6 ( 𝑦 ∈ ℕ → ( 𝜒𝜃 ) )
8 1nn 1 ∈ ℕ
9 2 elrab ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 1 ∈ ℕ ∧ 𝜓 ) )
10 8 6 9 mpbir2an 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
11 elrabi ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑦 ∈ ℕ )
12 peano2nn ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
13 12 a1d ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ ) )
14 13 7 anim12d ( 𝑦 ∈ ℕ → ( ( 𝑦 ∈ ℕ ∧ 𝜒 ) → ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) ) )
15 3 elrab ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ ∧ 𝜒 ) )
16 4 elrab ( ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) )
17 14 15 16 3imtr4g ( 𝑦 ∈ ℕ → ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) )
18 11 17 mpcom ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } )
19 18 rgen 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
20 nfcv 𝑦
21 1 20 nfrabw 𝑦 { 𝑥 ∈ ℕ ∣ 𝜑 }
22 nfcv 𝑤 { 𝑥 ∈ ℕ ∣ 𝜑 }
23 nfv 𝑤 ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
24 21 nfel2 𝑦 ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
25 oveq1 ( 𝑦 = 𝑤 → ( 𝑦 + 1 ) = ( 𝑤 + 1 ) )
26 25 eleq1d ( 𝑦 = 𝑤 → ( ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) )
27 21 22 23 24 26 cbvralfw ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ∀ 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } )
28 19 27 mpbi 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
29 peano5nni ( ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) → ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 } )
30 10 28 29 mp2an ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 }
31 30 sseli ( 𝐴 ∈ ℕ → 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } )
32 5 elrab ( 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝐴 ∈ ℕ ∧ 𝜏 ) )
33 31 32 sylib ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℕ ∧ 𝜏 ) )
34 33 simprd ( 𝐴 ∈ ℕ → 𝜏 )