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 |
|
cofu2.h |
|- H = ( Hom ` C ) |
7 |
|
cofu2.y |
|- ( ph -> R e. ( X H Y ) ) |
8 |
1 2 3 4 5
|
cofu2nd |
|- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ) |
9 |
8
|
fveq1d |
|- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) ) |
10 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
11 |
|
relfunc |
|- Rel ( C Func D ) |
12 |
|
1st2ndbr |
|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
13 |
11 2 12
|
sylancr |
|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) |
14 |
1 6 10 13 4 5
|
funcf2 |
|- ( ph -> ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) ) |
15 |
|
fvco3 |
|- ( ( ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) /\ R e. ( X H Y ) ) -> ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) ) |
16 |
14 7 15
|
syl2anc |
|- ( ph -> ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) ) |
17 |
9 16
|
eqtrd |
|- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) ) |