Step |
Hyp |
Ref |
Expression |
1 |
|
iswlkg.v |
|- V = ( Vtx ` G ) |
2 |
|
iswlkg.i |
|- I = ( iEdg ` G ) |
3 |
|
wlkv |
|- ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) |
4 |
|
3simpc |
|- ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) ) |
5 |
3 4
|
syl |
|- ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) ) |
6 |
5
|
a1i |
|- ( G e. W -> ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) ) ) |
7 |
|
elex |
|- ( F e. Word dom I -> F e. _V ) |
8 |
|
ovex |
|- ( 0 ... ( # ` F ) ) e. _V |
9 |
1
|
fvexi |
|- V e. _V |
10 |
8 9
|
fpm |
|- ( P : ( 0 ... ( # ` F ) ) --> V -> P e. ( V ^pm ( 0 ... ( # ` F ) ) ) ) |
11 |
10
|
elexd |
|- ( P : ( 0 ... ( # ` F ) ) --> V -> P e. _V ) |
12 |
7 11
|
anim12i |
|- ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( F e. _V /\ P e. _V ) ) |
13 |
12
|
3adant3 |
|- ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( F e. _V /\ P e. _V ) ) |
14 |
13
|
a1i |
|- ( G e. W -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( F e. _V /\ P e. _V ) ) ) |
15 |
1 2
|
iswlk |
|- ( ( G e. W /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) ) |
16 |
15
|
3expib |
|- ( G e. W -> ( ( F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) ) ) |
17 |
6 14 16
|
pm5.21ndd |
|- ( G e. W -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) ) |