Theorem wlkiswwlks2lem2

Description: Lemma 2 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

	Ref	Expression
Hypothesis	wlkiswwlks2lem.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
Assertion	wlkiswwlks2lem2	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( 𝐹 ‘ 𝐼 ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks2lem.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
2		fveq2	⊢ ( 𝑥 = 𝐼 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐼 ) )
3		fvoveq1	⊢ ( 𝑥 = 𝐼 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
4	2 3	preq12d	⊢ ( 𝑥 = 𝐼 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } )
5	4	fveq2d	⊢ ( 𝑥 = 𝐼 → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )
6		simpr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
7		fvexd	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) ∈ V )
8	1 5 6 7	fvmptd3	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( 𝐹 ‘ 𝐼 ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝐼 ) , ( 𝑃 ‘ ( 𝐼 + 1 ) ) } ) )