Metamath Proof Explorer

Theorem elwspths2on

Description: A simple path of length 2 between two vertices (in a graph) as length 3 string. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 16-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 elwwlks2on.v 
 |-  V = ( Vtx ` G )
2 wspthnon 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. f f ( A ( SPathsOn ` G ) C ) W ) )
3 2 biimpi 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. f f ( A ( SPathsOn ` G ) C ) W ) )
4 1 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 ) ) ) )
5 simpl 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> W = <" A b C "> )
6 eleq1 
 |-  ( W = <" A b C "> -> ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
7 6 biimpa 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) )
8 5 7 jca 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
9 8 ex 
 |-  ( W = <" A b C "> -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
10 9 adantr 
 |-  ( ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
11 10 com12 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
12 11 reximdv 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
13 12 a1i13 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( E. f f ( A ( SPathsOn ` G ) C ) W -> ( E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
14 13 com24 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) -> ( E. f f ( A ( SPathsOn ` G ) C ) W -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
15 4 14 sylbid 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( E. f f ( A ( SPathsOn ` G ) C ) W -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
16 15 impd 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. f f ( A ( SPathsOn ` G ) C ) W ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) )
17 16 com23 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. f f ( A ( SPathsOn ` G ) C ) W ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) )
18 3 17 mpdi 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
19 6 biimpar 
 |-  ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) )
20 19 a1i 
 |-  ( ( ( G e. UPGraph /\ A e. V /\ C e. V ) /\ b e. V ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) ) )
21 20 rexlimdva 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) ) )
22 18 21 impbid 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )