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 |
|
cofu2nd.x |
|- ( ph -> X e. B ) |
5 |
|
cofu2nd.y |
|- ( ph -> Y e. B ) |
6 |
1 2 3
|
cofuval |
|- ( 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 ) ) ) >. ) |
7 |
6
|
fveq2d |
|- ( ph -> ( 2nd ` ( G o.func F ) ) = ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) ) |
8 |
|
fvex |
|- ( 1st ` G ) e. _V |
9 |
|
fvex |
|- ( 1st ` F ) e. _V |
10 |
8 9
|
coex |
|- ( ( 1st ` G ) o. ( 1st ` F ) ) e. _V |
11 |
1
|
fvexi |
|- B e. _V |
12 |
11 11
|
mpoex |
|- ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) e. _V |
13 |
10 12
|
op2nd |
|- ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 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 ) ) ) |
14 |
7 13
|
eqtrdi |
|- ( ph -> ( 2nd ` ( G o.func F ) ) = ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) ) |
15 |
|
simprl |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X ) |
16 |
15
|
fveq2d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` X ) ) |
17 |
|
simprr |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y ) |
18 |
17
|
fveq2d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( 1st ` F ) ` y ) = ( ( 1st ` F ) ` Y ) ) |
19 |
16 18
|
oveq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) = ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ) |
20 |
15 17
|
oveq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x ( 2nd ` F ) y ) = ( X ( 2nd ` F ) Y ) ) |
21 |
19 20
|
coeq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( ( ( 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 ) ) ) |
22 |
|
ovex |
|- ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) e. _V |
23 |
|
ovex |
|- ( X ( 2nd ` F ) Y ) e. _V |
24 |
22 23
|
coex |
|- ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) e. _V |
25 |
24
|
a1i |
|- ( ph -> ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) e. _V ) |
26 |
14 21 4 5 25
|
ovmpod |
|- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ) |