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 )