Metamath Proof Explorer

Theorem curf2

Description: Value of the curry functor at a morphism. (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 )
Assertion curf2 
|- ( ph -> L = ( z e. B |-> ( 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 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
14 eqid 
 |-  ( Id ` C ) = ( Id ` C )
15 1 2 3 4 5 6 13 14 7 8 curfval 
 |-  ( ph -> G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` 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 ) ) ) ) ) >. )
16 2 fvexi 
 |-  A e. _V
17 16 mptex 
 |-  ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) e. _V
18 16 16 mpoex 
 |-  ( 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
19 17 18 op2ndd 
 |-  ( G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` 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 ) ) ) ) ) >. -> ( 2nd ` G ) = ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) )
20 15 19 syl 
 |-  ( ph -> ( 2nd ` G ) = ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) )
21 10 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. A )
22 ovex 
 |-  ( x H y ) e. _V
23 22 mptex 
 |-  ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) e. _V
24 23 a1i 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) e. _V )
25 11 adantr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> K e. ( X H Y ) )
26 simprl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
27 simprr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
28 26 27 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x H y ) = ( X H Y ) )
29 25 28 eleqtrrd 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> K e. ( x H y ) )
30 6 fvexi 
 |-  B e. _V
31 30 mptex 
 |-  ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) e. _V
32 31 a1i 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) e. _V )
33 simplrl 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> x = X )
34 33 opeq1d 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> <. x , z >. = <. X , z >. )
35 simplrr 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> y = Y )
36 35 opeq1d 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> <. y , z >. = <. Y , z >. )
37 34 36 oveq12d 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> ( <. x , z >. ( 2nd ` F ) <. y , z >. ) = ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) )
38 simpr 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> g = K )
39 eqidd 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> ( I ` z ) = ( I ` z ) )
40 37 38 39 oveq123d 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) = ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) )
41 40 mpteq2dv 
 |-  ( ( ( ph /\ ( x = X /\ y = Y ) ) /\ g = K ) -> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )
42 29 32 41 fvmptdv2 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( X ( 2nd ` G ) Y ) = ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) ) )
43 9 21 24 42 ovmpodv 
 |-  ( ph -> ( ( 2nd ` G ) = ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) ) )
44 20 43 mpd 
 |-  ( ph -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )
45 12 44 syl5eq 
 |-  ( ph -> L = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )