Step |
Hyp |
Ref |
Expression |
1 |
|
wlkcomp.v |
|- V = ( Vtx ` G ) |
2 |
|
wlkcomp.i |
|- I = ( iEdg ` G ) |
3 |
|
wlkcomp.1 |
|- F = ( 1st ` W ) |
4 |
|
wlkcomp.2 |
|- P = ( 2nd ` W ) |
5 |
3
|
eqcomi |
|- ( 1st ` W ) = F |
6 |
4
|
eqcomi |
|- ( 2nd ` W ) = P |
7 |
5 6
|
pm3.2i |
|- ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P ) |
8 |
|
eqop |
|- ( W e. ( S X. T ) -> ( W = <. F , P >. <-> ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P ) ) ) |
9 |
7 8
|
mpbiri |
|- ( W e. ( S X. T ) -> W = <. F , P >. ) |
10 |
9
|
eleq1d |
|- ( W e. ( S X. T ) -> ( W e. ( Walks ` G ) <-> <. F , P >. e. ( Walks ` G ) ) ) |
11 |
|
df-br |
|- ( F ( Walks ` G ) P <-> <. F , P >. e. ( Walks ` G ) ) |
12 |
10 11
|
bitr4di |
|- ( W e. ( S X. T ) -> ( W e. ( Walks ` G ) <-> F ( Walks ` G ) P ) ) |
13 |
1 2
|
iswlkg |
|- ( G e. U -> ( 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 ) ) ) ) ) ) |
14 |
12 13
|
sylan9bbr |
|- ( ( G e. U /\ W e. ( S X. T ) ) -> ( W e. ( Walks ` G ) <-> ( 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 ) ) ) ) ) ) |