Metamath Proof Explorer

Theorem upgrwlkcompim

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

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

Proof

Step Hyp Ref Expression
1 upgrwlkcompim.v 
 |-  V = ( Vtx ` G )
2 upgrwlkcompim.i 
 |-  I = ( iEdg ` G )
3 upgrwlkcompim.1 
 |-  F = ( 1st ` W )
4 upgrwlkcompim.2 
 |-  P = ( 2nd ` W )
5 wlkcpr 
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
6 3 4 breq12i 
 |-  ( F ( Walks ` G ) P <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
7 5 6 bitr4i 
 |-  ( W e. ( Walks ` G ) <-> F ( Walks ` G ) P )
8 1 2 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
9 8 biimpd 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
10 7 9 syl5bi 
 |-  ( G e. UPGraph -> ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
11 10 imp 
 |-  ( ( G e. UPGraph /\ W e. ( Walks ` G ) ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )