Step |
Hyp |
Ref |
Expression |
1 |
|
2clwwlk.c |
⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) |
2 |
1
|
2clwwlk |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) |
3 |
2
|
eleq2d |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ) ) |
4 |
|
fveq1 |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ ( 𝑁 − 2 ) ) ) |
5 |
4
|
eqeq1d |
⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) |
6 |
5
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∣ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 } ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) |
7 |
3 6
|
bitrdi |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) |