Metamath Proof Explorer

Theorem precofval

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

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

Proof

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