Step |
Hyp |
Ref |
Expression |
1 |
|
wlkop |
⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ) |
2 |
|
wlkvv |
⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → 𝑊 ∈ ( V × V ) ) |
3 |
|
1st2ndb |
⊢ ( 𝑊 ∈ ( V × V ) ↔ 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ) |
4 |
2 3
|
sylib |
⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ) |
5 |
|
eleq1 |
⊢ ( 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 → ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ∈ ( Walks ‘ 𝐺 ) ) ) |
6 |
|
df-br |
⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) ↔ 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ∈ ( Walks ‘ 𝐺 ) ) |
7 |
5 6
|
bitr4di |
⊢ ( 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 → ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) ) ) |
8 |
1 4 7
|
pm5.21nii |
⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) ) |