Metamath Proof Explorer

Theorem upgrwlkvtxedg

Description: The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Hypothesis wlkvtxedg.e 
|- E = ( Edg ` G )
Assertion upgrwlkvtxedg 
|- ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )

Proof

Step Hyp Ref Expression
1 wlkvtxedg.e 
 |-  E = ( Edg ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
5 3 1 upgredginwlk 
 |-  ( ( G e. UPGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. E ) )
6 5 ancoms 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. E ) )
7 6 imp 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) e. E )
8 eleq1 
 |-  ( { ( P ` k ) , ( P ` ( k + 1 ) ) } = ( ( iEdg ` G ) ` ( F ` k ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( ( iEdg ` G ) ` ( F ` k ) ) e. E ) )
9 8 eqcoms 
 |-  ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( ( iEdg ` G ) ` ( F ` k ) ) e. E ) )
10 7 9 syl5ibrcom 
 |-  ( ( ( F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
11 10 ralimdva 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
12 11 impancom 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( G e. UPGraph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
13 12 3adant2 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( G e. UPGraph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
14 13 com12 
 |-  ( G e. UPGraph -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
15 4 14 sylbid 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
16 15 imp 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )