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	⊢ ( 𝐴 ∈ ℕ → 𝜏 )

Metamath Proof Explorer

Theorem nnindf

Proof