Step |
Hyp |
Ref |
Expression |
1 |
|
eupths.i |
|- I = ( iEdg ` G ) |
2 |
1
|
eupthi |
|- ( F ( EulerPaths ` G ) P -> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) ) |
3 |
2
|
simpld |
|- ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P ) |
4 |
1
|
wlkvtxeledg |
|- ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) |
5 |
|
fveq2 |
|- ( k = N -> ( P ` k ) = ( P ` N ) ) |
6 |
|
fvoveq1 |
|- ( k = N -> ( P ` ( k + 1 ) ) = ( P ` ( N + 1 ) ) ) |
7 |
5 6
|
preq12d |
|- ( k = N -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) |
8 |
|
2fveq3 |
|- ( k = N -> ( I ` ( F ` k ) ) = ( I ` ( F ` N ) ) ) |
9 |
7 8
|
sseq12d |
|- ( k = N -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) ) |
10 |
9
|
rspccv |
|- ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( N e. ( 0 ..^ ( # ` F ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) ) |
11 |
3 4 10
|
3syl |
|- ( F ( EulerPaths ` G ) P -> ( N e. ( 0 ..^ ( # ` F ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) ) |
12 |
11
|
imp |
|- ( ( F ( EulerPaths ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) |