Step |
Hyp |
Ref |
Expression |
1 |
|
wksfval.v |
|- V = ( Vtx ` G ) |
2 |
|
wksfval.i |
|- I = ( iEdg ` G ) |
3 |
|
df-br |
|- ( F ( Walks ` G ) P <-> <. F , P >. e. ( Walks ` G ) ) |
4 |
1 2
|
wksfval |
|- ( G e. W -> ( Walks ` G ) = { <. f , 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 ) ) ) ) } ) |
5 |
4
|
3ad2ant1 |
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( Walks ` G ) = { <. f , 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 ) ) ) ) } ) |
6 |
5
|
eleq2d |
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( <. F , P >. e. ( Walks ` G ) <-> <. F , P >. e. { <. f , 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 ) ) ) ) } ) ) |
7 |
3 6
|
syl5bb |
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> <. F , P >. e. { <. f , 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 ) ) ) ) } ) ) |
8 |
|
eleq1 |
|- ( f = F -> ( f e. Word dom I <-> F e. Word dom I ) ) |
9 |
8
|
adantr |
|- ( ( f = F /\ p = P ) -> ( f e. Word dom I <-> F e. Word dom I ) ) |
10 |
|
simpr |
|- ( ( f = F /\ p = P ) -> p = P ) |
11 |
|
fveq2 |
|- ( f = F -> ( # ` f ) = ( # ` F ) ) |
12 |
11
|
oveq2d |
|- ( f = F -> ( 0 ... ( # ` f ) ) = ( 0 ... ( # ` F ) ) ) |
13 |
12
|
adantr |
|- ( ( f = F /\ p = P ) -> ( 0 ... ( # ` f ) ) = ( 0 ... ( # ` F ) ) ) |
14 |
10 13
|
feq12d |
|- ( ( f = F /\ p = P ) -> ( p : ( 0 ... ( # ` f ) ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) ) |
15 |
11
|
oveq2d |
|- ( f = F -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( # ` F ) ) ) |
16 |
15
|
adantr |
|- ( ( f = F /\ p = P ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( # ` F ) ) ) |
17 |
|
fveq1 |
|- ( p = P -> ( p ` k ) = ( P ` k ) ) |
18 |
|
fveq1 |
|- ( p = P -> ( p ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) |
19 |
17 18
|
eqeq12d |
|- ( p = P -> ( ( p ` k ) = ( p ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) ) |
20 |
19
|
adantl |
|- ( ( f = F /\ p = P ) -> ( ( p ` k ) = ( p ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) ) |
21 |
|
fveq1 |
|- ( f = F -> ( f ` k ) = ( F ` k ) ) |
22 |
21
|
fveq2d |
|- ( f = F -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) ) |
23 |
17
|
sneqd |
|- ( p = P -> { ( p ` k ) } = { ( P ` k ) } ) |
24 |
22 23
|
eqeqan12d |
|- ( ( f = F /\ p = P ) -> ( ( I ` ( f ` k ) ) = { ( p ` k ) } <-> ( I ` ( F ` k ) ) = { ( P ` k ) } ) ) |
25 |
17 18
|
preq12d |
|- ( p = P -> { ( p ` k ) , ( p ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) |
26 |
25
|
adantl |
|- ( ( f = F /\ p = P ) -> { ( p ` k ) , ( p ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) |
27 |
22
|
adantr |
|- ( ( f = F /\ p = P ) -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) ) |
28 |
26 27
|
sseq12d |
|- ( ( f = F /\ p = P ) -> ( { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) |
29 |
20 24 28
|
ifpbi123d |
|- ( ( f = F /\ p = P ) -> ( if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) |
30 |
16 29
|
raleqbidv |
|- ( ( f = F /\ p = P ) -> ( 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 ) ) ) <-> 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 ) ) ) ) ) |
31 |
9 14 30
|
3anbi123d |
|- ( ( f = F /\ p = 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 ) ) ) ) <-> ( 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 ) ) ) ) ) ) |
32 |
31
|
opelopabga |
|- ( ( F e. U /\ P e. Z ) -> ( <. F , P >. e. { <. f , 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) ) |
33 |
32
|
3adant1 |
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( <. F , P >. e. { <. f , 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) ) |
34 |
7 33
|
bitrd |
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( 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 ) ) ) ) ) ) |