Metamath Proof Explorer

Theorem tposcurf12

Description: The partially evaluated transposed curry functor at a morphism. (Contributed by Zhi Wang, 9-Oct-2025)

Ref Expression
Hypotheses tposcurf1.g 
|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
tposcurf1.a 
|- A = ( Base ` C )
tposcurf1.c 
|- ( ph -> C e. Cat )
tposcurf1.d 
|- ( ph -> D e. Cat )
tposcurf1.f 
|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
tposcurf1.x 
|- ( ph -> X e. A )
tposcurf1.k 
|- ( ph -> K = ( ( 1st ` G ) ` X ) )
tposcurf1.b 
|- B = ( Base ` D )
tposcurf11.y 
|- ( ph -> Y e. B )
tposcurf12.j 
|- J = ( Hom ` D )
tposcurf12.1 
|- .1. = ( Id ` C )
tposcurf12.y 
|- ( ph -> Z e. B )
tposcurf12.g 
|- ( ph -> H e. ( Y J Z ) )
Assertion tposcurf12 
|- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( H ( <. Y , X >. ( 2nd ` F ) <. Z , X >. ) ( .1. ` X ) ) )

Proof

Step Hyp Ref Expression
1 tposcurf1.g 
 |-  ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
2 tposcurf1.a 
 |-  A = ( Base ` C )
3 tposcurf1.c 
 |-  ( ph -> C e. Cat )
4 tposcurf1.d 
 |-  ( ph -> D e. Cat )
5 tposcurf1.f 
 |-  ( ph -> F e. ( ( D Xc. C ) Func E ) )
6 tposcurf1.x 
 |-  ( ph -> X e. A )
7 tposcurf1.k 
 |-  ( ph -> K = ( ( 1st ` G ) ` X ) )
8 tposcurf1.b 
 |-  B = ( Base ` D )
9 tposcurf11.y 
 |-  ( ph -> Y e. B )
10 tposcurf12.j 
 |-  J = ( Hom ` D )
11 tposcurf12.1 
 |-  .1. = ( Id ` C )
12 tposcurf12.y 
 |-  ( ph -> Z e. B )
13 tposcurf12.g 
 |-  ( ph -> H e. ( Y J Z ) )
14 1 fveq2d 
 |-  ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
16 7 15 eqtrd 
 |-  ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
17 16 fveq2d 
 |-  ( ph -> ( 2nd ` K ) = ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) )
18 17 oveqd 
 |-  ( ph -> ( Y ( 2nd ` K ) Z ) = ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) )
19 18 fveq1d 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) )
20 eqid 
 |-  ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
21 eqidd 
 |-  ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
22 3 4 5 21 cofuswapfcl 
 |-  ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
23 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X )
24 20 2 3 4 22 8 6 23 9 10 11 12 13 curf12 
 |-  ( ph -> ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) )
25 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
26 2 25 11 3 6 catidcl 
 |-  ( ph -> ( .1. ` X ) e. ( X ( Hom ` C ) X ) )
27 3 4 5 21 2 8 6 9 6 12 25 10 26 13 cofuswapf2 
 |-  ( ph -> ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) = ( H ( <. Y , X >. ( 2nd ` F ) <. Z , X >. ) ( .1. ` X ) ) )
28 19 24 27 3eqtrd 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( H ( <. Y , X >. ( 2nd ` F ) <. Z , X >. ) ( .1. ` X ) ) )