Metamath Proof Explorer

Theorem prcoftposcurfuco

Description: The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025)

Ref Expression
Hypotheses prcoffunc.r 
|- R = ( D FuncCat E )
prcoffunc.e 
|- ( ph -> E e. Cat )
prcoftposcurfuco.q 
|- Q = ( C FuncCat D )
prcoftposcurfuco.o 
|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
prcoftposcurfuco.m 
|- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) )
prcoftposcurfuco.f 
|- ( ph -> F ( C Func D ) G )
Assertion prcoftposcurfuco 
|- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = M )

Proof

Step Hyp Ref Expression
1 prcoffunc.r 
 |-  R = ( D FuncCat E )
2 prcoffunc.e 
 |-  ( ph -> E e. Cat )
3 prcoftposcurfuco.q 
 |-  Q = ( C FuncCat D )
4 prcoftposcurfuco.o 
 |-  ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
5 prcoftposcurfuco.m 
 |-  ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) )
6 prcoftposcurfuco.f 
 |-  ( ph -> F ( C Func D ) G )
7 eqid 
 |-  ( D Func E ) = ( D Func E )
8 eqid 
 |-  ( D Nat E ) = ( D Nat E )
9 6 funcrcl3 
 |-  ( ph -> D e. Cat )
10 relfunc 
 |-  Rel ( C Func D )
11 7 8 9 2 10 6 prcofval 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) >. )
12 eqidd 
 |-  ( ph -> ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) = ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) )
13 eqidd 
 |-  ( ph -> ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) )
14 1 7 8 6 2 12 13 3 4 5 precofval3 
 |-  ( ph -> <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) >. = M )
15 11 14 eqtrd 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = M )