Step |
Hyp |
Ref |
Expression |
1 |
|
cofuval.b |
|- B = ( Base ` C ) |
2 |
|
cofuval.f |
|- ( ph -> F e. ( C Func D ) ) |
3 |
|
cofuval.g |
|- ( ph -> G e. ( D Func E ) ) |
4 |
|
df-cofu |
|- o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) |
5 |
4
|
a1i |
|- ( ph -> o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) ) |
6 |
|
simprl |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> g = G ) |
7 |
6
|
fveq2d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( 1st ` g ) = ( 1st ` G ) ) |
8 |
|
simprr |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> f = F ) |
9 |
8
|
fveq2d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( 1st ` f ) = ( 1st ` F ) ) |
10 |
7 9
|
coeq12d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` g ) o. ( 1st ` f ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) ) |
11 |
8
|
fveq2d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` f ) = ( 2nd ` F ) ) |
12 |
11
|
dmeqd |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` f ) = dom ( 2nd ` F ) ) |
13 |
|
relfunc |
|- Rel ( C Func D ) |
14 |
|
1st2ndbr |
|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
15 |
13 2 14
|
sylancr |
|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
16 |
1 15
|
funcfn2 |
|- ( ph -> ( 2nd ` F ) Fn ( B X. B ) ) |
17 |
16
|
fndmd |
|- ( ph -> dom ( 2nd ` F ) = ( B X. B ) ) |
18 |
17
|
adantr |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` F ) = ( B X. B ) ) |
19 |
12 18
|
eqtrd |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` f ) = ( B X. B ) ) |
20 |
19
|
dmeqd |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> dom dom ( 2nd ` f ) = dom ( B X. B ) ) |
21 |
|
dmxpid |
|- dom ( B X. B ) = B |
22 |
20 21
|
eqtrdi |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> dom dom ( 2nd ` f ) = B ) |
23 |
6
|
fveq2d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` g ) = ( 2nd ` G ) ) |
24 |
9
|
fveq1d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` x ) ) |
25 |
9
|
fveq1d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` f ) ` y ) = ( ( 1st ` F ) ` y ) ) |
26 |
23 24 25
|
oveq123d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) = ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) ) |
27 |
11
|
oveqd |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( x ( 2nd ` f ) y ) = ( x ( 2nd ` F ) y ) ) |
28 |
26 27
|
coeq12d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) |
29 |
22 22 28
|
mpoeq123dv |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) = ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) ) |
30 |
10 29
|
opeq12d |
|- ( ( ph /\ ( g = G /\ f = F ) ) -> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) |
31 |
3
|
elexd |
|- ( ph -> G e. _V ) |
32 |
2
|
elexd |
|- ( ph -> F e. _V ) |
33 |
|
opex |
|- <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. e. _V |
34 |
33
|
a1i |
|- ( ph -> <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. e. _V ) |
35 |
5 30 31 32 34
|
ovmpod |
|- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) |