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