Metamath Proof Explorer

Theorem wlkcompim

Description: Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Hypotheses wlkcomp.v 
|- V = ( Vtx ` G )
wlkcomp.i 
|- I = ( iEdg ` G )
wlkcomp.1 
|- F = ( 1st ` W )
wlkcomp.2 
|- P = ( 2nd ` W )
Assertion wlkcompim 
|- ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkcomp.v 
 |-  V = ( Vtx ` G )
2 wlkcomp.i 
 |-  I = ( iEdg ` G )
3 wlkcomp.1 
 |-  F = ( 1st ` W )
4 wlkcomp.2 
 |-  P = ( 2nd ` W )
5 elfvex 
 |-  ( W e. ( Walks ` G ) -> G e. _V )
6 wlkcpr 
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
7 wlkvv 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> W e. ( _V X. _V ) )
8 6 7 sylbi 
 |-  ( W e. ( Walks ` G ) -> W e. ( _V X. _V ) )
9 1 2 3 4 wlkcomp 
 |-  ( ( G e. _V /\ W e. ( _V X. _V ) ) -> ( W e. ( Walks ` G ) <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
10 9 biimpcd 
 |-  ( W e. ( Walks ` G ) -> ( ( G e. _V /\ W e. ( _V X. _V ) ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
11 5 8 10 mp2and 
 |-  ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )