Metamath Proof Explorer

Theorem tposcurf11

Description: Value of the double evaluated transposed curry functor. (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 )
Assertion tposcurf11 
|- ( ph -> ( ( 1st ` K ) ` Y ) = ( Y ( 1st ` F ) 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 1 fveq2d 
 |-  ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
12 7 11 eqtrd 
 |-  ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
13 12 fveq2d 
 |-  ( ph -> ( 1st ` K ) = ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) )
14 13 fveq1d 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) )
15 eqid 
 |-  ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
16 eqidd 
 |-  ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
17 3 4 5 16 cofuswapfcl 
 |-  ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
18 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X )
19 15 2 3 4 17 8 6 18 9 curf11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) )
20 3 4 5 16 2 8 6 9 cofuswapf1 
 |-  ( ph -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) = ( Y ( 1st ` F ) X ) )
21 14 19 20 3eqtrd 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = ( Y ( 1st ` F ) X ) )