Metamath Proof Explorer

Theorem tposcurf2cl

Description: The transposed curry functor at a morphism is a natural transformation. (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 ) )
tposcurf2.n 
|- N = ( D Nat E )
Assertion tposcurf2cl 
|- ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )

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 tposcurf2.n 
 |-  N = ( D Nat E )
14 eqid 
 |-  ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
15 eqidd 
 |-  ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
16 3 4 5 15 cofuswapfcl 
 |-  ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
17 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 )
18 14 2 3 4 16 6 7 8 9 10 11 17 13 curf2cl 
 |-  ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) e. ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) )
19 1 fveq2d 
 |-  ( ph -> ( 2nd ` G ) = ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
20 19 oveqd 
 |-  ( ph -> ( X ( 2nd ` G ) Y ) = ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) )
21 20 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) )
22 12 21 eqtrd 
 |-  ( ph -> L = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) )
23 1 fveq2d 
 |-  ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
24 23 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
25 23 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` Y ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) )
26 24 25 oveq12d 
 |-  ( ph -> ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) = ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) )
27 18 22 26 3eltr4d 
 |-  ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )