Metamath Proof Explorer

Theorem tposcurf2

Description: Value of the transposed curry functor at a morphism. (Contributed by Zhi Wang, 10-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 tposcurf2.g 
 |-  ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
2 tposcurf2.a 
 |-  A = ( Base ` C )
3 tposcurf2.c 
 |-  ( ph -> C e. Cat )
4 tposcurf2.d 
 |-  ( ph -> D e. Cat )
5 tposcurf2.f 
 |-  ( ph -> F e. ( ( D Xc. C ) Func E ) )
6 tposcurf2.b 
 |-  B = ( Base ` D )
7 tposcurf2.h 
 |-  H = ( Hom ` C )
8 tposcurf2.i 
 |-  I = ( Id ` D )
9 tposcurf2.x 
 |-  ( ph -> X e. A )
10 tposcurf2.y 
 |-  ( ph -> Y e. A )
11 tposcurf2.k 
 |-  ( ph -> K e. ( X H Y ) )
12 tposcurf2.l 
 |-  ( ph -> L = ( ( X ( 2nd ` G ) Y ) ` K ) )
13 1 fveq2d 
 |-  ( ph -> ( 2nd ` G ) = ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
14 13 oveqd 
 |-  ( ph -> ( X ( 2nd ` G ) Y ) = ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) )
15 14 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) )
16 12 15 eqtrd 
 |-  ( ph -> L = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) )
17 eqid 
 |-  ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
18 eqidd 
 |-  ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
19 3 4 5 18 cofuswapfcl 
 |-  ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
20 eqid 
 |-  ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K )
21 17 2 3 4 19 6 7 8 9 10 11 20 curf2 
 |-  ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) )
22 3 adantr 
 |-  ( ( ph /\ z e. B ) -> C e. Cat )
23 4 adantr 
 |-  ( ( ph /\ z e. B ) -> D e. Cat )
24 5 adantr 
 |-  ( ( ph /\ z e. B ) -> F e. ( ( D Xc. C ) Func E ) )
25 eqidd 
 |-  ( ( ph /\ z e. B ) -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
26 9 adantr 
 |-  ( ( ph /\ z e. B ) -> X e. A )
27 simpr 
 |-  ( ( ph /\ z e. B ) -> z e. B )
28 10 adantr 
 |-  ( ( ph /\ z e. B ) -> Y e. A )
29 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
30 11 adantr 
 |-  ( ( ph /\ z e. B ) -> K e. ( X H Y ) )
31 6 29 8 23 27 catidcl 
 |-  ( ( ph /\ z e. B ) -> ( I ` z ) e. ( z ( Hom ` D ) z ) )
32 22 23 24 25 2 6 26 27 28 27 7 29 30 31 cofuswapf2 
 |-  ( ( ph /\ z e. B ) -> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) = ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) )
33 32 mpteq2dva 
 |-  ( ph -> ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) = ( z e. B |-> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) )
34 16 21 33 3eqtrd 
 |-  ( ph -> L = ( z e. B |-> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) )