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 
|- V = ( Vtx ` G )
Assertion wwlks2onsym 
|- ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> <" C B A "> e. ( C ( 2 WWalksNOn G ) A ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2on.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 umgrwwlks2on 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( { A , B } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) ) )
4 3anrev 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) <-> ( C e. V /\ B e. V /\ A e. V ) )
5 1 2 umgrwwlks2on 
 |-  ( ( G e. UMGraph /\ ( C e. V /\ B e. V /\ A e. V ) ) -> ( <" C B A "> e. ( C ( 2 WWalksNOn G ) A ) <-> ( { C , B } e. ( Edg ` G ) /\ { B , A } e. ( Edg ` G ) ) ) )
6 4 5 sylan2b 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" C B A "> e. ( C ( 2 WWalksNOn G ) A ) <-> ( { C , B } e. ( Edg ` G ) /\ { B , A } e. ( Edg ` G ) ) ) )
7 prcom 
 |-  { C , B } = { B , C }
8 7 eleq1i 
 |-  ( { C , B } e. ( Edg ` G ) <-> { B , C } e. ( Edg ` G ) )
9 prcom 
 |-  { B , A } = { A , B }
10 9 eleq1i 
 |-  ( { B , A } e. ( Edg ` G ) <-> { A , B } e. ( Edg ` G ) )
11 8 10 anbi12ci 
 |-  ( ( { C , B } e. ( Edg ` G ) /\ { B , A } e. ( Edg ` G ) ) <-> ( { A , B } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) )
12 6 11 bitr2di 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( { A , B } e. ( Edg ` G ) /\ { B , C } e. ( Edg ` G ) ) <-> <" C B A "> e. ( C ( 2 WWalksNOn G ) A ) ) )
13 3 12 bitrd 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> <" C B A "> e. ( C ( 2 WWalksNOn G ) A ) ) )