Step |
Hyp |
Ref |
Expression |
1 |
|
elwwlks2on.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
umgrwwlks2on |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
4 |
|
3anrev |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) |
5 |
1 2
|
umgrwwlks2on |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( 〈“ 𝐶 𝐵 𝐴 ”〉 ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
6 |
4 5
|
sylan2b |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 〈“ 𝐶 𝐵 𝐴 ”〉 ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ↔ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
7 |
|
prcom |
⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 } |
8 |
7
|
eleq1i |
⊢ ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) |
9 |
|
prcom |
⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 } |
10 |
9
|
eleq1i |
⊢ ( { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ) |
11 |
8 10
|
anbi12ci |
⊢ ( ( { 𝐶 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ) |
12 |
6 11
|
bitr2di |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ) ↔ 〈“ 𝐶 𝐵 𝐴 ”〉 ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) ) |
13 |
3 12
|
bitrd |
⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ 〈“ 𝐶 𝐵 𝐴 ”〉 ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) ) |