Metamath Proof Explorer

Theorem tposcurf1

Description: Value of the object part of the 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 )
tposcurf1.j 
|- J = ( Hom ` D )
tposcurf1.1 
|- .1. = ( Id ` C )
Assertion tposcurf1 
|- ( ph -> K = <. ( y e. B |-> ( y ( 1st ` F ) X ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. 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 tposcurf1.j 
 |-  J = ( Hom ` D )
10 tposcurf1.1 
 |-  .1. = ( Id ` C )
11 1 fveq2d 
 |-  ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
12 11 fveq1d 
 |-  ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
13 eqid 
 |-  ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
14 eqidd 
 |-  ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
15 3 4 5 14 cofuswapfcl 
 |-  ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
16 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X )
17 13 2 3 4 15 8 6 16 9 10 curf1 
 |-  ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. )
18 7 12 17 3eqtrd 
 |-  ( ph -> K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. )
19 8 fvexi 
 |-  B e. _V
20 19 mptex 
 |-  ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) e. _V
21 19 19 mpoex 
 |-  ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) e. _V
22 20 21 op1std 
 |-  ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) )
23 18 22 syl 
 |-  ( ph -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) )
24 ovexd 
 |-  ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) e. _V )
25 23 24 fvmpt2d 
 |-  ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) )
26 1 adantr 
 |-  ( ( ph /\ y e. B ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
27 3 adantr 
 |-  ( ( ph /\ y e. B ) -> C e. Cat )
28 4 adantr 
 |-  ( ( ph /\ y e. B ) -> D e. Cat )
29 5 adantr 
 |-  ( ( ph /\ y e. B ) -> F e. ( ( D Xc. C ) Func E ) )
30 6 adantr 
 |-  ( ( ph /\ y e. B ) -> X e. A )
31 7 adantr 
 |-  ( ( ph /\ y e. B ) -> K = ( ( 1st ` G ) ` X ) )
32 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
33 26 2 27 28 29 30 31 8 32 tposcurf11 
 |-  ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( y ( 1st ` F ) X ) )
34 25 33 eqtr3d 
 |-  ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) = ( y ( 1st ` F ) X ) )
35 34 mpteq2dva 
 |-  ( ph -> ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) = ( y e. B |-> ( y ( 1st ` F ) X ) ) )
36 20 21 op2ndd 
 |-  ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) )
37 18 36 syl 
 |-  ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) )
38 ovex 
 |-  ( y J z ) e. _V
39 38 mptex 
 |-  ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V
40 39 a1i 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V )
41 37 40 ovmpt4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( 2nd ` K ) z ) = ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) )
42 ovexd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) e. _V )
43 41 42 fvmpt2d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) )
44 1 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
45 3 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> C e. Cat )
46 4 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> D e. Cat )
47 5 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> F e. ( ( D Xc. C ) Func E ) )
48 6 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> X e. A )
49 7 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> K = ( ( 1st ` G ) ` X ) )
50 simplrl 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> y e. B )
51 simplrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> z e. B )
52 simpr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> g e. ( y J z ) )
53 44 2 45 46 47 48 49 8 50 9 10 51 52 tposcurf12 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) )
54 43 53 eqtr3d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) = ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) )
55 54 mpteq2dva 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) )
56 55 3impb 
 |-  ( ( ph /\ y e. B /\ z e. B ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) )
57 56 mpoeq3dva 
 |-  ( ph -> ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) )
58 35 57 opeq12d 
 |-  ( ph -> <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. = <. ( y e. B |-> ( y ( 1st ` F ) X ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) >. )
59 18 58 eqtrd 
 |-  ( ph -> K = <. ( y e. B |-> ( y ( 1st ` F ) X ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) >. )