Metamath Proof Explorer

Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g 
|- G = ( <. C , D >. curryF F )
curf2.a 
|- A = ( Base ` C )
curf2.c 
|- ( ph -> C e. Cat )
curf2.d 
|- ( ph -> D e. Cat )
curf2.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
curf2.b 
|- B = ( Base ` D )
curf2.h 
|- H = ( Hom ` C )
curf2.i 
|- I = ( Id ` D )
curf2.x 
|- ( ph -> X e. A )
curf2.y 
|- ( ph -> Y e. A )
curf2.k 
|- ( ph -> K e. ( X H Y ) )
curf2.l 
|- L = ( ( X ( 2nd ` G ) Y ) ` K )
curf2.z 
|- ( ph -> Z e. B )
Assertion curf2val 
|- ( ph -> ( L ` Z ) = ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) )

Proof

Step Hyp Ref Expression
1 curf2.g 
 |-  G = ( <. C , D >. curryF F )
2 curf2.a 
 |-  A = ( Base ` C )
3 curf2.c 
 |-  ( ph -> C e. Cat )
4 curf2.d 
 |-  ( ph -> D e. Cat )
5 curf2.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
6 curf2.b 
 |-  B = ( Base ` D )
7 curf2.h 
 |-  H = ( Hom ` C )
8 curf2.i 
 |-  I = ( Id ` D )
9 curf2.x 
 |-  ( ph -> X e. A )
10 curf2.y 
 |-  ( ph -> Y e. A )
11 curf2.k 
 |-  ( ph -> K e. ( X H Y ) )
12 curf2.l 
 |-  L = ( ( X ( 2nd ` G ) Y ) ` K )
13 curf2.z 
 |-  ( ph -> Z e. B )
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 
 |-  ( ph -> L = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )
15 simpr 
 |-  ( ( ph /\ z = Z ) -> z = Z )
16 15 opeq2d 
 |-  ( ( ph /\ z = Z ) -> <. X , z >. = <. X , Z >. )
17 15 opeq2d 
 |-  ( ( ph /\ z = Z ) -> <. Y , z >. = <. Y , Z >. )
18 16 17 oveq12d 
 |-  ( ( ph /\ z = Z ) -> ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) = ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) )
19 eqidd 
 |-  ( ( ph /\ z = Z ) -> K = K )
20 15 fveq2d 
 |-  ( ( ph /\ z = Z ) -> ( I ` z ) = ( I ` Z ) )
21 18 19 20 oveq123d 
 |-  ( ( ph /\ z = Z ) -> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) = ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) )
22 ovexd 
 |-  ( ph -> ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) e. _V )
23 14 21 13 22 fvmptd 
 |-  ( ph -> ( L ` Z ) = ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) )