Metamath Proof Explorer

Theorem postcofval

Description: Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025)

Ref Expression
Hypotheses postcofval.q 
|- Q = ( C FuncCat D )
postcofval.r 
|- R = ( D FuncCat E )
postcofval.o 
|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
postcofval.f 
|- ( ph -> F e. ( D Func E ) )
postcofval.c 
|- ( ph -> C e. Cat )
postcofval.k 
|- K = ( ( 1st ` .o. ) ` F )
Assertion postcofval 
|- ( ph -> K = <. ( g e. ( C Func D ) |-> ( F o.func g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 postcofval.q 
 |-  Q = ( C FuncCat D )
2 postcofval.r 
 |-  R = ( D FuncCat E )
3 postcofval.o 
 |-  .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
4 postcofval.f 
 |-  ( ph -> F e. ( D Func E ) )
5 postcofval.c 
 |-  ( ph -> C e. Cat )
6 postcofval.k 
 |-  K = ( ( 1st ` .o. ) ` F )
7 2 fucbas 
 |-  ( D Func E ) = ( Base ` R )
8 4 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
9 8 funcrcl2 
 |-  ( ph -> D e. Cat )
10 8 funcrcl3 
 |-  ( ph -> E e. Cat )
11 2 9 10 fuccat 
 |-  ( ph -> R e. Cat )
12 1 5 9 fuccat 
 |-  ( ph -> Q e. Cat )
13 2 1 oveq12i 
 |-  ( R Xc. Q ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
14 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
15 13 14 5 9 10 fucofunca 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) )
16 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
17 eqid 
 |-  ( C Nat D ) = ( C Nat D )
18 1 17 fuchom 
 |-  ( C Nat D ) = ( Hom ` Q )
19 eqid 
 |-  ( Id ` R ) = ( Id ` R )
20 3 7 11 12 15 16 4 6 18 19 curf1 
 |-  ( ph -> K = <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. )
21 eqidd 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> ( 1st ` ( <. C , D >. o.F E ) ) = ( 1st ` ( <. C , D >. o.F E ) ) )
22 simpr 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> g e. ( C Func D ) )
23 4 adantr 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> F e. ( D Func E ) )
24 21 22 23 fuco11b 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) = ( F o.func g ) )
25 24 mpteq2dva 
 |-  ( ph -> ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) = ( g e. ( C Func D ) |-> ( F o.func g ) ) )
26 eqidd 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( 2nd ` ( <. C , D >. o.F E ) ) = ( 2nd ` ( <. C , D >. o.F E ) ) )
27 simpr 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> a e. ( g ( C Nat D ) h ) )
28 4 adantr 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> F e. ( D Func E ) )
29 26 19 2 27 28 fucolid 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) )
30 29 mpteq2dva 
 |-  ( ph -> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) = ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) )
31 30 mpoeq3dv 
 |-  ( ph -> ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) = ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) )
32 25 31 opeq12d 
 |-  ( ph -> <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. = <. ( g e. ( C Func D ) |-> ( F o.func g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) >. )
33 20 32 eqtrd 
 |-  ( ph -> K = <. ( g e. ( C Func D ) |-> ( F o.func g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) >. )