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 relfunc 
 |-  Rel ( D Func E )
9 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
10 8 4 9 sylancr 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
11 10 funcrcl2 
 |-  ( ph -> D e. Cat )
12 10 funcrcl3 
 |-  ( ph -> E e. Cat )
13 2 11 12 fuccat 
 |-  ( ph -> R e. Cat )
14 1 5 11 fuccat 
 |-  ( ph -> Q e. Cat )
15 2 1 oveq12i 
 |-  ( R Xc. Q ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
16 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
17 15 16 5 11 12 fucofunca 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) )
18 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
19 eqid 
 |-  ( C Nat D ) = ( C Nat D )
20 1 19 fuchom 
 |-  ( C Nat D ) = ( Hom ` Q )
21 eqid 
 |-  ( Id ` R ) = ( Id ` R )
22 3 7 13 14 17 18 4 6 20 21 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 ) ) ) >. )
23 eqidd 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> ( 1st ` ( <. C , D >. o.F E ) ) = ( 1st ` ( <. C , D >. o.F E ) ) )
24 simpr 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> g e. ( C Func D ) )
25 4 adantr 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> F e. ( D Func E ) )
26 23 24 25 fuco11b 
 |-  ( ( ph /\ g e. ( C Func D ) ) -> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) = ( F o.func g ) )
27 26 mpteq2dva 
 |-  ( ph -> ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) = ( g e. ( C Func D ) |-> ( F o.func g ) ) )
28 eqidd 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( 2nd ` ( <. C , D >. o.F E ) ) = ( 2nd ` ( <. C , D >. o.F E ) ) )
29 simpr 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> a e. ( g ( C Nat D ) h ) )
30 4 adantr 
 |-  ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> F e. ( D Func E ) )
31 28 21 2 29 30 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 ) ) ) )
32 31 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 ) ) ) ) )
33 32 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 ) ) ) ) ) )
34 27 33 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 ) ) ) ) ) >. )
35 22 34 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 ) ) ) ) ) >. )