This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) } ) )