Metamath Proof Explorer

Theorem curfval

Description: Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses curfval.g 
|- G = ( <. C , D >. curryF F )
curfval.a 
|- A = ( Base ` C )
curfval.c 
|- ( ph -> C e. Cat )
curfval.d 
|- ( ph -> D e. Cat )
curfval.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
curfval.b 
|- B = ( Base ` D )
curfval.j 
|- J = ( Hom ` D )
curfval.1 
|- .1. = ( Id ` C )
curfval.h 
|- H = ( Hom ` C )
curfval.i 
|- I = ( Id ` D )
Assertion curfval 
|- ( 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 ) ) ) ) ) >. )

Proof

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 eqtrid 
 |-  ( 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 ) ) ) ) ) >. )