MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  curfval Structured version   Unicode version

Theorem curfval 15045
Description: Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
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  X.c  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
Ref Expression
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 ) ) ) ) ) >. )
Distinct variable groups:    x, g,
y, z,  .1.    x, A, y    B, g, x, y, z    C, g, x, y, z    D, g, x, y, z    g, H, y, z    ph, g, x, y, z    g, E, y, z    g, J, x   
g, F, x, y, z
Allowed substitution hints:    A( z, g)    E( x)    G( x, y, z, g)    H( x)    I( x, y, z, g)    J( y, z)

Proof of Theorem curfval
Dummy variables  c 
d  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 curfval.g . 2  |-  G  =  ( <. C ,  D >. curryF  F
)
2 df-curf 15036 . . . 4  |- 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 ) ) ) ) ) >. )
32a1i 11 . . 3  |-  ( 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 ) ) ) ) ) >. )
)
4 fvex 5713 . . . . 5  |-  ( 1st `  e )  e.  _V
54a1i 11 . . . 4  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  ( 1st `  e )  e. 
_V )
6 simprl 755 . . . . . 6  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  e  =  <. C ,  D >. )
76fveq2d 5707 . . . . 5  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  ( 1st `  e )  =  ( 1st `  <. C ,  D >. )
)
8 curfval.c . . . . . . 7  |-  ( ph  ->  C  e.  Cat )
9 curfval.d . . . . . . 7  |-  ( ph  ->  D  e.  Cat )
10 op1stg 6601 . . . . . . 7  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  ( 1st `  <. C ,  D >. )  =  C )
118, 9, 10syl2anc 661 . . . . . 6  |-  ( ph  ->  ( 1st `  <. C ,  D >. )  =  C )
1211adantr 465 . . . . 5  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  ( 1st `  <. C ,  D >. )  =  C )
137, 12eqtrd 2475 . . . 4  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  ( 1st `  e )  =  C )
14 fvex 5713 . . . . . 6  |-  ( 2nd `  e )  e.  _V
1514a1i 11 . . . . 5  |-  ( ( ( ph  /\  (
e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  ->  ( 2nd `  e
)  e.  _V )
166adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  (
e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  ->  e  =  <. C ,  D >. )
1716fveq2d 5707 . . . . . 6  |-  ( ( ( ph  /\  (
e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  ->  ( 2nd `  e
)  =  ( 2nd `  <. C ,  D >. ) )
18 op2ndg 6602 . . . . . . . 8  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  ( 2nd `  <. C ,  D >. )  =  D )
198, 9, 18syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( 2nd `  <. C ,  D >. )  =  D )
2019ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  (
e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  ->  ( 2nd `  <. C ,  D >. )  =  D )
2117, 20eqtrd 2475 . . . . 5  |-  ( ( ( ph  /\  (
e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  ->  ( 2nd `  e
)  =  D )
22 simplr 754 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  c  =  C )
2322fveq2d 5707 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Base `  c )  =  (
Base `  C )
)
24 curfval.a . . . . . . . 8  |-  A  =  ( Base `  C
)
2523, 24syl6eqr 2493 . . . . . . 7  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Base `  c )  =  A )
26 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  d  =  D )
2726fveq2d 5707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Base `  d )  =  (
Base `  D )
)
28 curfval.b . . . . . . . . . 10  |-  B  =  ( Base `  D
)
2927, 28syl6eqr 2493 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Base `  d )  =  B )
30 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  ->  f  =  F )
3130ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  f  =  F )
3231fveq2d 5707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( 1st `  f )  =  ( 1st `  F ) )
3332oveqd 6120 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( x
( 1st `  f
) y )  =  ( x ( 1st `  F ) y ) )
3429, 33mpteq12dv 4382 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
3526fveq2d 5707 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Hom  `  d )  =  ( Hom  `  D )
)
36 curfval.j . . . . . . . . . . . 12  |-  J  =  ( Hom  `  D
)
3735, 36syl6eqr 2493 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Hom  `  d )  =  J )
3837oveqd 6120 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( y
( Hom  `  d ) z )  =  ( y J z ) )
3931fveq2d 5707 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( 2nd `  f )  =  ( 2nd `  F ) )
4039oveqd 6120 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( <. x ,  y >. ( 2nd `  f ) <.
x ,  z >.
)  =  ( <.
x ,  y >.
( 2nd `  F
) <. x ,  z
>. ) )
4122fveq2d 5707 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Id `  c )  =  ( Id `  C ) )
42 curfval.1 . . . . . . . . . . . . 13  |-  .1.  =  ( Id `  C )
4341, 42syl6eqr 2493 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Id `  c )  =  .1.  )
4443fveq1d 5705 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( ( Id `  c ) `  x )  =  (  .1.  `  x )
)
45 eqidd 2444 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  g  =  g )
4640, 44, 45oveq123d 6124 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
4738, 46mpteq12dv 4382 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
4829, 29, 47mpt2eq123dv 6160 . . . . . . . 8  |-  ( ( ( ( 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 ) ) ) )
4934, 48opeq12d 4079 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) >. )
5025, 49mpteq12dv 4382 . . . . . 6  |-  ( ( ( ( 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 ) ) ) >. ) )
5122fveq2d 5707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Hom  `  c )  =  ( Hom  `  C )
)
52 curfval.h . . . . . . . . . 10  |-  H  =  ( Hom  `  C
)
5351, 52syl6eqr 2493 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Hom  `  c )  =  H )
5453oveqd 6120 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( x
( Hom  `  c ) y )  =  ( x H y ) )
5539oveqd 6120 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( <. x ,  z >. ( 2nd `  f ) <.
y ,  z >.
)  =  ( <.
x ,  z >.
( 2nd `  F
) <. y ,  z
>. ) )
5626fveq2d 5707 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Id `  d )  =  ( Id `  D ) )
57 curfval.i . . . . . . . . . . . 12  |-  I  =  ( Id `  D
)
5856, 57syl6eqr 2493 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( Id `  d )  =  I )
5958fveq1d 5705 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  =  <. C ,  D >.  /\  f  =  F ) )  /\  c  =  C )  /\  d  =  D
)  ->  ( ( Id `  d ) `  z )  =  ( I `  z ) )
6055, 45, 59oveq123d 6124 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
6129, 60mpteq12dv 4382 . . . . . . . 8  |-  ( ( ( ( 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 ) ) ) )
6254, 61mpteq12dv 4382 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) ) )
6325, 25, 62mpt2eq123dv 6160 . . . . . 6  |-  ( ( ( ( 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 ) ) ) ) ) )
6450, 63opeq12d 4079 . . . . 5  |-  ( ( ( ( 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 ) ) ) ) ) >. )
6515, 21, 64csbied2 3327 . . . 4  |-  ( ( ( 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 ) ) ) ) ) >. )
665, 13, 65csbied2 3327 . . 3  |-  ( (
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 ) ) ) ) ) >. )
67 opex 4568 . . . 4  |-  <. C ,  D >.  e.  _V
6867a1i 11 . . 3  |-  ( ph  -> 
<. C ,  D >.  e. 
_V )
69 curfval.f . . . 4  |-  ( ph  ->  F  e.  ( ( C  X.c  D )  Func  E
) )
70 elex 2993 . . . 4  |-  ( F  e.  ( ( C  X.c  D )  Func  E
)  ->  F  e.  _V )
7169, 70syl 16 . . 3  |-  ( ph  ->  F  e.  _V )
72 opex 4568 . . . 4  |-  <. (
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
7372a1i 11 . . 3  |-  ( 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 )
743, 66, 68, 71, 73ovmpt2d 6230 . 2  |-  ( 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 ) ) ) ) ) >. )
751, 74syl5eq 2487 1  |-  ( 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 ) ) ) ) ) >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2984   [_csb 3300   <.cop 3895    e. cmpt 4362   ` cfv 5430  (class class class)co 6103    e. cmpt2 6105   1stc1st 6587   2ndc2nd 6588   Basecbs 14186   Hom chom 14261   Catccat 14614   Idccid 14615    Func cfunc 14776    X.c cxpc 14990   curryF ccurf 15032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-iota 5393  df-fun 5432  df-fv 5438  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-1st 6589  df-2nd 6590  df-curf 15036
This theorem is referenced by:  curf1fval  15046  curf2  15051  curfcl  15054  curfpropd  15055  curfuncf  15060
  Copyright terms: Public domain W3C validator