Step |
Hyp |
Ref |
Expression |
1 |
|
uncfval.g |
|- F = ( <" C D E "> uncurryF G ) |
2 |
|
uncfval.c |
|- ( ph -> D e. Cat ) |
3 |
|
uncfval.d |
|- ( ph -> E e. Cat ) |
4 |
|
uncfval.f |
|- ( ph -> G e. ( C Func ( D FuncCat E ) ) ) |
5 |
|
uncf1.a |
|- A = ( Base ` C ) |
6 |
|
uncf1.b |
|- B = ( Base ` D ) |
7 |
|
uncf1.x |
|- ( ph -> X e. A ) |
8 |
|
uncf1.y |
|- ( ph -> Y e. B ) |
9 |
1 2 3 4
|
uncfval |
|- ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) |
10 |
9
|
fveq2d |
|- ( ph -> ( 1st ` F ) = ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) ) |
11 |
10
|
oveqd |
|- ( ph -> ( X ( 1st ` F ) Y ) = ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) ) |
12 |
|
df-ov |
|- ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) = ( ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) ` <. X , Y >. ) |
13 |
|
eqid |
|- ( C Xc. D ) = ( C Xc. D ) |
14 |
13 5 6
|
xpcbas |
|- ( A X. B ) = ( Base ` ( C Xc. D ) ) |
15 |
|
eqid |
|- ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) = ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) |
16 |
|
eqid |
|- ( ( D FuncCat E ) Xc. D ) = ( ( D FuncCat E ) Xc. D ) |
17 |
|
funcrcl |
|- ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) ) |
18 |
4 17
|
syl |
|- ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) ) |
19 |
18
|
simpld |
|- ( ph -> C e. Cat ) |
20 |
|
eqid |
|- ( C 1stF D ) = ( C 1stF D ) |
21 |
13 19 2 20
|
1stfcl |
|- ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) ) |
22 |
21 4
|
cofucl |
|- ( ph -> ( G o.func ( C 1stF D ) ) e. ( ( C Xc. D ) Func ( D FuncCat E ) ) ) |
23 |
|
eqid |
|- ( C 2ndF D ) = ( C 2ndF D ) |
24 |
13 19 2 23
|
2ndfcl |
|- ( ph -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) ) |
25 |
15 16 22 24
|
prfcl |
|- ( ph -> ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) e. ( ( C Xc. D ) Func ( ( D FuncCat E ) Xc. D ) ) ) |
26 |
|
eqid |
|- ( D evalF E ) = ( D evalF E ) |
27 |
|
eqid |
|- ( D FuncCat E ) = ( D FuncCat E ) |
28 |
26 27 2 3
|
evlfcl |
|- ( ph -> ( D evalF E ) e. ( ( ( D FuncCat E ) Xc. D ) Func E ) ) |
29 |
7 8
|
opelxpd |
|- ( ph -> <. X , Y >. e. ( A X. B ) ) |
30 |
14 25 28 29
|
cofu1 |
|- ( ph -> ( ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) ` <. X , Y >. ) = ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) ) |
31 |
12 30
|
syl5eq |
|- ( ph -> ( X ( 1st ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) Y ) = ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) ) |
32 |
|
eqid |
|- ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) ) |
33 |
15 14 32 22 24 29
|
prf1 |
|- ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. ) |
34 |
14 21 4 29
|
cofu1 |
|- ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) ) |
35 |
13 14 32 19 2 20 29
|
1stf1 |
|- ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = ( 1st ` <. X , Y >. ) ) |
36 |
|
op1stg |
|- ( ( X e. A /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X ) |
37 |
7 8 36
|
syl2anc |
|- ( ph -> ( 1st ` <. X , Y >. ) = X ) |
38 |
35 37
|
eqtrd |
|- ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = X ) |
39 |
38
|
fveq2d |
|- ( ph -> ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` G ) ` X ) ) |
40 |
34 39
|
eqtrd |
|- ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` X ) ) |
41 |
13 14 32 19 2 23 29
|
2ndf1 |
|- ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = ( 2nd ` <. X , Y >. ) ) |
42 |
|
op2ndg |
|- ( ( X e. A /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y ) |
43 |
7 8 42
|
syl2anc |
|- ( ph -> ( 2nd ` <. X , Y >. ) = Y ) |
44 |
41 43
|
eqtrd |
|- ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = Y ) |
45 |
40 44
|
opeq12d |
|- ( ph -> <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. = <. ( ( 1st ` G ) ` X ) , Y >. ) |
46 |
33 45
|
eqtrd |
|- ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` G ) ` X ) , Y >. ) |
47 |
46
|
fveq2d |
|- ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( 1st ` ( D evalF E ) ) ` <. ( ( 1st ` G ) ` X ) , Y >. ) ) |
48 |
|
df-ov |
|- ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) = ( ( 1st ` ( D evalF E ) ) ` <. ( ( 1st ` G ) ` X ) , Y >. ) |
49 |
47 48
|
eqtr4di |
|- ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) ) |
50 |
27
|
fucbas |
|- ( D Func E ) = ( Base ` ( D FuncCat E ) ) |
51 |
|
relfunc |
|- Rel ( C Func ( D FuncCat E ) ) |
52 |
|
1st2ndbr |
|- ( ( Rel ( C Func ( D FuncCat E ) ) /\ G e. ( C Func ( D FuncCat E ) ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) ) |
53 |
51 4 52
|
sylancr |
|- ( ph -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) ) |
54 |
5 50 53
|
funcf1 |
|- ( ph -> ( 1st ` G ) : A --> ( D Func E ) ) |
55 |
54 7
|
ffvelrnd |
|- ( ph -> ( ( 1st ` G ) ` X ) e. ( D Func E ) ) |
56 |
26 2 3 6 55 8
|
evlf1 |
|- ( ph -> ( ( ( 1st ` G ) ` X ) ( 1st ` ( D evalF E ) ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) ) |
57 |
49 56
|
eqtrd |
|- ( ph -> ( ( 1st ` ( D evalF E ) ) ` ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) ) |
58 |
11 31 57
|
3eqtrd |
|- ( ph -> ( X ( 1st ` F ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) ) |