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