Step |
Hyp |
Ref |
Expression |
1 |
|
diagval.l |
|- L = ( C DiagFunc D ) |
2 |
|
diagval.c |
|- ( ph -> C e. Cat ) |
3 |
|
diagval.d |
|- ( ph -> D e. Cat ) |
4 |
|
diag11.a |
|- A = ( Base ` C ) |
5 |
|
diag11.c |
|- ( ph -> X e. A ) |
6 |
|
diag11.k |
|- K = ( ( 1st ` L ) ` X ) |
7 |
|
diag11.b |
|- B = ( Base ` D ) |
8 |
|
diag11.y |
|- ( ph -> Y e. B ) |
9 |
1 2 3
|
diagval |
|- ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) ) |
10 |
9
|
fveq2d |
|- ( ph -> ( 1st ` L ) = ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ) |
11 |
10
|
fveq1d |
|- ( ph -> ( ( 1st ` L ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) |
12 |
6 11
|
eqtrid |
|- ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) |
13 |
12
|
fveq2d |
|- ( ph -> ( 1st ` K ) = ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) ) |
14 |
13
|
fveq1d |
|- ( ph -> ( ( 1st ` K ) ` Y ) = ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) ` Y ) ) |
15 |
|
eqid |
|- ( <. C , D >. curryF ( C 1stF D ) ) = ( <. C , D >. curryF ( C 1stF D ) ) |
16 |
|
eqid |
|- ( C Xc. D ) = ( C Xc. D ) |
17 |
|
eqid |
|- ( C 1stF D ) = ( C 1stF D ) |
18 |
16 2 3 17
|
1stfcl |
|- ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) ) |
19 |
|
eqid |
|- ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) |
20 |
15 4 2 3 18 7 5 19 8
|
curf11 |
|- ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) ` Y ) = ( X ( 1st ` ( C 1stF D ) ) Y ) ) |
21 |
|
df-ov |
|- ( X ( 1st ` ( C 1stF D ) ) Y ) = ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) |
22 |
16 4 7
|
xpcbas |
|- ( A X. B ) = ( Base ` ( C Xc. D ) ) |
23 |
|
eqid |
|- ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) ) |
24 |
5 8
|
opelxpd |
|- ( ph -> <. X , Y >. e. ( A X. B ) ) |
25 |
16 22 23 2 3 17 24
|
1stf1 |
|- ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = ( 1st ` <. X , Y >. ) ) |
26 |
21 25
|
eqtrid |
|- ( ph -> ( X ( 1st ` ( C 1stF D ) ) Y ) = ( 1st ` <. X , Y >. ) ) |
27 |
|
op1stg |
|- ( ( X e. A /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X ) |
28 |
5 8 27
|
syl2anc |
|- ( ph -> ( 1st ` <. X , Y >. ) = X ) |
29 |
26 28
|
eqtrd |
|- ( ph -> ( X ( 1st ` ( C 1stF D ) ) Y ) = X ) |
30 |
14 20 29
|
3eqtrd |
|- ( ph -> ( ( 1st ` K ) ` Y ) = X ) |