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

Metamath Proof Explorer

Theorem elwwlks2on

Description: A walk of length 2 between two vertices as length 3 string. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis elwwlks2on.v 
|- V = ( Vtx ` G )
Assertion elwwlks2on 
|- ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2on.v 
 |-  V = ( Vtx ` G )
2 1 elwwlks2ons3 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
3 1 s3wwlks2on 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) ) )
4 breq2 
 |-  ( <" A b C "> = W -> ( f ( Walks ` G ) <" A b C "> <-> f ( Walks ` G ) W ) )
5 4 eqcoms 
 |-  ( W = <" A b C "> -> ( f ( Walks ` G ) <" A b C "> <-> f ( Walks ` G ) W ) )
6 5 anbi1d 
 |-  ( W = <" A b C "> -> ( ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) <-> ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) )
7 6 exbidv 
 |-  ( W = <" A b C "> -> ( E. f ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) <-> E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) )
8 3 7 sylan9bb 
 |-  ( ( ( G e. UPGraph /\ A e. V /\ C e. V ) /\ W = <" A b C "> ) -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) )
9 8 pm5.32da 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) )
10 9 rexbidv 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) )
11 2 10 bitrid 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) )