Step |
Hyp |
Ref |
Expression |
1 |
|
curfval.g |
|- G = ( <. C , D >. curryF F ) |
2 |
|
curfval.a |
|- A = ( Base ` C ) |
3 |
|
curfval.c |
|- ( ph -> C e. Cat ) |
4 |
|
curfval.d |
|- ( ph -> D e. Cat ) |
5 |
|
curfval.f |
|- ( ph -> F e. ( ( C Xc. D ) Func E ) ) |
6 |
|
curfval.b |
|- B = ( Base ` D ) |
7 |
|
curfval.j |
|- J = ( Hom ` D ) |
8 |
|
curfval.1 |
|- .1. = ( Id ` C ) |
9 |
|
curfval.h |
|- H = ( Hom ` C ) |
10 |
|
curfval.i |
|- I = ( Id ` D ) |
11 |
|
df-curf |
|- curryF = ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. ) |
12 |
11
|
a1i |
|- ( ph -> curryF = ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. ) ) |
13 |
|
fvexd |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> ( 1st ` e ) e. _V ) |
14 |
|
simprl |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> e = <. C , D >. ) |
15 |
14
|
fveq2d |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> ( 1st ` e ) = ( 1st ` <. C , D >. ) ) |
16 |
|
op1stg |
|- ( ( C e. Cat /\ D e. Cat ) -> ( 1st ` <. C , D >. ) = C ) |
17 |
3 4 16
|
syl2anc |
|- ( ph -> ( 1st ` <. C , D >. ) = C ) |
18 |
17
|
adantr |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> ( 1st ` <. C , D >. ) = C ) |
19 |
15 18
|
eqtrd |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> ( 1st ` e ) = C ) |
20 |
|
fvexd |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> ( 2nd ` e ) e. _V ) |
21 |
14
|
adantr |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> e = <. C , D >. ) |
22 |
21
|
fveq2d |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> ( 2nd ` e ) = ( 2nd ` <. C , D >. ) ) |
23 |
|
op2ndg |
|- ( ( C e. Cat /\ D e. Cat ) -> ( 2nd ` <. C , D >. ) = D ) |
24 |
3 4 23
|
syl2anc |
|- ( ph -> ( 2nd ` <. C , D >. ) = D ) |
25 |
24
|
ad2antrr |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> ( 2nd ` <. C , D >. ) = D ) |
26 |
22 25
|
eqtrd |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> ( 2nd ` e ) = D ) |
27 |
|
simplr |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> c = C ) |
28 |
27
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Base ` c ) = ( Base ` C ) ) |
29 |
28 2
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Base ` c ) = A ) |
30 |
|
simpr |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> d = D ) |
31 |
30
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Base ` d ) = ( Base ` D ) ) |
32 |
31 6
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Base ` d ) = B ) |
33 |
|
simprr |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> f = F ) |
34 |
33
|
ad2antrr |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> f = F ) |
35 |
34
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( 1st ` f ) = ( 1st ` F ) ) |
36 |
35
|
oveqd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( x ( 1st ` f ) y ) = ( x ( 1st ` F ) y ) ) |
37 |
32 36
|
mpteq12dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) = ( y e. B |-> ( x ( 1st ` F ) y ) ) ) |
38 |
30
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Hom ` d ) = ( Hom ` D ) ) |
39 |
38 7
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Hom ` d ) = J ) |
40 |
39
|
oveqd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( y ( Hom ` d ) z ) = ( y J z ) ) |
41 |
34
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( 2nd ` f ) = ( 2nd ` F ) ) |
42 |
41
|
oveqd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( <. x , y >. ( 2nd ` f ) <. x , z >. ) = ( <. x , y >. ( 2nd ` F ) <. x , z >. ) ) |
43 |
27
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Id ` c ) = ( Id ` C ) ) |
44 |
43 8
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Id ` c ) = .1. ) |
45 |
44
|
fveq1d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( ( Id ` c ) ` x ) = ( .1. ` x ) ) |
46 |
|
eqidd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> g = g ) |
47 |
42 45 46
|
oveq123d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) = ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) |
48 |
40 47
|
mpteq12dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) = ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) |
49 |
32 32 48
|
mpoeq123dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) ) |
50 |
37 49
|
opeq12d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. = <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) |
51 |
29 50
|
mpteq12dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) = ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) ) |
52 |
27
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Hom ` c ) = ( Hom ` C ) ) |
53 |
52 9
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Hom ` c ) = H ) |
54 |
53
|
oveqd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( x ( Hom ` c ) y ) = ( x H y ) ) |
55 |
41
|
oveqd |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( <. x , z >. ( 2nd ` f ) <. y , z >. ) = ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ) |
56 |
30
|
fveq2d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Id ` d ) = ( Id ` D ) ) |
57 |
56 10
|
eqtr4di |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( Id ` d ) = I ) |
58 |
57
|
fveq1d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( ( Id ` d ) ` z ) = ( I ` z ) ) |
59 |
55 46 58
|
oveq123d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) = ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) |
60 |
32 59
|
mpteq12dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) = ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) |
61 |
54 60
|
mpteq12dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) = ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) |
62 |
29 29 61
|
mpoeq123dv |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) = ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) ) |
63 |
51 62
|
opeq12d |
|- ( ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) /\ d = D ) -> <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. ) |
64 |
20 26 63
|
csbied2 |
|- ( ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) /\ c = C ) -> [_ ( 2nd ` e ) / d ]_ <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. ) |
65 |
13 19 64
|
csbied2 |
|- ( ( ph /\ ( e = <. C , D >. /\ f = F ) ) -> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. ) |
66 |
|
opex |
|- <. C , D >. e. _V |
67 |
66
|
a1i |
|- ( ph -> <. C , D >. e. _V ) |
68 |
5
|
elexd |
|- ( ph -> F e. _V ) |
69 |
|
opex |
|- <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. e. _V |
70 |
69
|
a1i |
|- ( ph -> <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. e. _V ) |
71 |
12 65 67 68 70
|
ovmpod |
|- ( ph -> ( <. C , D >. curryF F ) = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. ) |
72 |
1 71
|
syl5eq |
|- ( ph -> G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. ) |