This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkvtxedg

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

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

Proof

Step Hyp Ref Expression
1 wlkvtxedg.e 
 |-  E = ( Edg ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 2 wlkvtxiedg 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran ( iEdg ` G ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
4 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 1 4 eqtr2i 
 |-  ran ( iEdg ` G ) = E
6 5 rexeqi 
 |-  ( E. e e. ran ( iEdg ` G ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> E. e e. E { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
7 6 ralbii 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran ( iEdg ` G ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. E { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
8 3 7 sylib 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. E { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )