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 ) |