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