Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlkovh.h |
⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) |
2 |
|
oveq12 |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
3 |
|
oveq1 |
⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 2 ) = ( 𝑁 − 2 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑛 − 2 ) = ( 𝑁 − 2 ) ) |
5 |
4
|
fveq2d |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( 𝑤 ‘ ( 𝑛 − 2 ) ) = ( 𝑤 ‘ ( 𝑁 − 2 ) ) ) |
6 |
|
simpl |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → 𝑣 = 𝑋 ) |
7 |
5 6
|
neeq12d |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → ( ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 ↔ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 ) ) |
8 |
2 7
|
rabeqbidv |
⊢ ( ( 𝑣 = 𝑋 ∧ 𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ) |
9 |
|
ovex |
⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ V |
10 |
9
|
rabex |
⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ∈ V |
11 |
8 1 10
|
ovmpoa |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) ≠ 𝑋 } ) |