Metamath Proof Explorer

Theorem elwwlks2ons3

Description: For each walk of length 2 between two vertices, there is a third vertex in the middle of the walk. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v 
|- V = ( Vtx ` G )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 wwlks2onv.v 
 |-  V = ( Vtx ` G )
2 id 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> W e. ( A ( 2 WWalksNOn G ) C ) )
3 1 elwwlks2ons3im 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) )
4 anass 
 |-  ( ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) <-> ( W e. ( A ( 2 WWalksNOn G ) C ) /\ ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) )
5 2 3 4 sylanbrc 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) )
6 simpr 
 |-  ( ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) -> ( W ` 1 ) e. V )
7 s3eq2 
 |-  ( b = ( W ` 1 ) -> <" A b C "> = <" A ( W ` 1 ) C "> )
8 eqeq2 
 |-  ( <" A b C "> = <" A ( W ` 1 ) C "> -> ( W = <" A b C "> <-> W = <" A ( W ` 1 ) C "> ) )
9 eleq1 
 |-  ( <" A b C "> = <" A ( W ` 1 ) C "> -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
10 8 9 anbi12d 
 |-  ( <" A b C "> = <" A ( W ` 1 ) C "> -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( W = <" A ( W ` 1 ) C "> /\ <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
11 7 10 syl 
 |-  ( b = ( W ` 1 ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( W = <" A ( W ` 1 ) C "> /\ <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
12 11 adantl 
 |-  ( ( ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) /\ b = ( W ` 1 ) ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( W = <" A ( W ` 1 ) C "> /\ <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
13 simpr 
 |-  ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) -> W = <" A ( W ` 1 ) C "> )
14 eleq1 
 |-  ( W = <" A ( W ` 1 ) C "> -> ( W e. ( A ( 2 WWalksNOn G ) C ) <-> <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
15 14 biimpac 
 |-  ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) -> <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) )
16 13 15 jca 
 |-  ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) -> ( W = <" A ( W ` 1 ) C "> /\ <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
17 16 adantr 
 |-  ( ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ <" A ( W ` 1 ) C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
18 6 12 17 rspcedvd 
 |-  ( ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ W = <" A ( W ` 1 ) C "> ) /\ ( W ` 1 ) e. V ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
19 5 18 syl 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) )
20 eleq1 
 |-  ( <" A b C "> = W -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> W e. ( A ( 2 WWalksNOn G ) C ) ) )
21 20 eqcoms 
 |-  ( W = <" A b C "> -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> W e. ( A ( 2 WWalksNOn G ) C ) ) )
22 21 biimpa 
 |-  ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> W e. ( A ( 2 WWalksNOn G ) C ) )
23 22 rexlimivw 
 |-  ( E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> W e. ( A ( 2 WWalksNOn G ) C ) )
24 19 23 impbii 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) )