Metamath Proof Explorer

Theorem curf1

Description: Value of the object part 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 )
curf1.x 
|- ( ph -> X e. A )
curf1.k 
|- K = ( ( 1st ` G ) ` X )
curf1.j 
|- J = ( Hom ` D )
curf1.1 
|- .1. = ( Id ` C )
Assertion curf1 
|- ( ph -> K = <. ( 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 ) ) ) >. )

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 curf1.x 
 |-  ( ph -> X e. A )
8 curf1.k 
 |-  K = ( ( 1st ` G ) ` X )
9 curf1.j 
 |-  J = ( Hom ` D )
10 curf1.1 
 |-  .1. = ( Id ` C )
11 1 2 3 4 5 6 9 10 curf1fval 
 |-  ( ph -> ( 1st ` 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 ) ) ) >. ) )
12 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
13 12 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x ( 1st ` F ) y ) = ( X ( 1st ` F ) y ) )
14 13 mpteq2dv 
 |-  ( ( ph /\ x = X ) -> ( y e. B |-> ( x ( 1st ` F ) y ) ) = ( y e. B |-> ( X ( 1st ` F ) y ) ) )
15 simp1r 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> x = X )
16 15 opeq1d 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> <. x , y >. = <. X , y >. )
17 15 opeq1d 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> <. x , z >. = <. X , z >. )
18 16 17 oveq12d 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> ( <. x , y >. ( 2nd ` F ) <. x , z >. ) = ( <. X , y >. ( 2nd ` F ) <. X , z >. ) )
19 15 fveq2d 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> ( .1. ` x ) = ( .1. ` X ) )
20 eqidd 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> g = g )
21 18 19 20 oveq123d 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) = ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) )
22 21 mpteq2dv 
 |-  ( ( ( ph /\ x = X ) /\ y e. B /\ z e. B ) -> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) = ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) )
23 22 mpoeq3dva 
 |-  ( ( ph /\ x = X ) -> ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` 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 ) ) ) )
24 14 23 opeq12d 
 |-  ( ( ph /\ x = X ) -> <. ( 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 ) ) ) >. = <. ( 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 ) ) ) >. )
25 opex 
 |-  <. ( 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 ) ) ) >. e. _V
26 25 a1i 
 |-  ( ph -> <. ( 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 ) ) ) >. e. _V )
27 11 24 7 26 fvmptd 
 |-  ( ph -> ( ( 1st ` G ) ` X ) = <. ( 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 ) ) ) >. )
28 8 27 eqtrid 
 |-  ( ph -> K = <. ( 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 ) ) ) >. )