This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlks2onsym

Description: There is a walk of length 2 from one vertex to another vertex iff there is a walk of length 2 from the other vertex to the first vertex. (Contributed by AV, 7-Jan-2022)

Ref Expression
Hypothesis elwwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wwlks2onsym ( ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( 𝐶 ( 2 WWalksNOn 𝐺 ) 𝐴 ) ) )

Proof

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 𝐺 ) 𝐴 ) ) )