Step |
Hyp |
Ref |
Expression |
1 |
|
wksonproplem.v |
|- V = ( Vtx ` G ) |
2 |
|
wksonproplem.b |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( W ` G ) B ) P <-> ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |
3 |
|
wksonproplem.d |
|- W = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( a ( O ` g ) b ) p /\ f ( Q ` g ) p ) } ) ) |
4 |
|
wksonproplem.w |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ f ( Q ` G ) p ) -> f ( Walks ` G ) p ) |
5 |
1
|
fvexi |
|- V e. _V |
6 |
|
simp1 |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> G e. _V ) |
7 |
|
simp2 |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> A e. V ) |
8 |
7 1
|
eleqtrdi |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> A e. ( Vtx ` G ) ) |
9 |
|
simp3 |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> B e. V ) |
10 |
9 1
|
eleqtrdi |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> B e. ( Vtx ` G ) ) |
11 |
|
wksv |
|- { <. f , p >. | f ( Walks ` G ) p } e. _V |
12 |
11
|
a1i |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> { <. f , p >. | f ( Walks ` G ) p } e. _V ) |
13 |
6 8 10 12 4 3
|
mptmpoopabovd |
|- ( ( G e. _V /\ A e. V /\ B e. V ) -> ( A ( W ` G ) B ) = { <. f , p >. | ( f ( A ( O ` G ) B ) p /\ f ( Q ` G ) p ) } ) |
14 |
|
fveq2 |
|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) ) |
15 |
14 1
|
eqtr4di |
|- ( g = G -> ( Vtx ` g ) = V ) |
16 |
|
fveq2 |
|- ( g = G -> ( O ` g ) = ( O ` G ) ) |
17 |
16
|
oveqd |
|- ( g = G -> ( a ( O ` g ) b ) = ( a ( O ` G ) b ) ) |
18 |
17
|
breqd |
|- ( g = G -> ( f ( a ( O ` g ) b ) p <-> f ( a ( O ` G ) b ) p ) ) |
19 |
|
fveq2 |
|- ( g = G -> ( Q ` g ) = ( Q ` G ) ) |
20 |
19
|
breqd |
|- ( g = G -> ( f ( Q ` g ) p <-> f ( Q ` G ) p ) ) |
21 |
18 20
|
anbi12d |
|- ( g = G -> ( ( f ( a ( O ` g ) b ) p /\ f ( Q ` g ) p ) <-> ( f ( a ( O ` G ) b ) p /\ f ( Q ` G ) p ) ) ) |
22 |
3 13 15 15 21
|
bropfvvvv |
|- ( ( V e. _V /\ V e. _V ) -> ( F ( A ( W ` G ) B ) P -> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) ) ) |
23 |
5 5 22
|
mp2an |
|- ( F ( A ( W ` G ) B ) P -> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) ) |
24 |
|
3anass |
|- ( ( G e. _V /\ A e. V /\ B e. V ) <-> ( G e. _V /\ ( A e. V /\ B e. V ) ) ) |
25 |
24
|
anbi1i |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( ( G e. _V /\ ( A e. V /\ B e. V ) ) /\ ( F e. _V /\ P e. _V ) ) ) |
26 |
|
df-3an |
|- ( ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( ( G e. _V /\ ( A e. V /\ B e. V ) ) /\ ( F e. _V /\ P e. _V ) ) ) |
27 |
25 26
|
bitr4i |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) <-> ( G e. _V /\ ( A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) ) |
28 |
23 27
|
sylibr |
|- ( F ( A ( W ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) ) |
29 |
2
|
biimpd |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( W ` G ) B ) P -> ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |
30 |
29
|
imdistani |
|- ( ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ F ( A ( W ` G ) B ) P ) -> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |
31 |
28 30
|
mpancom |
|- ( F ( A ( W ` G ) B ) P -> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |
32 |
|
df-3an |
|- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) <-> ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |
33 |
31 32
|
sylibr |
|- ( F ( A ( W ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) |