Metamath Proof Explorer

Theorem prcoftposcurfucoa

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 ) ) ) )
prcoftposcurfucoa.m 
|- ( ph -> M = ( ( 1st ` .o. ) ` F ) )
prcoftposcurfucoa.f 
|- ( ph -> F e. ( C Func D ) )
Assertion prcoftposcurfucoa 
|- ( ph -> ( <. D , E >. -o.F F ) = 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 prcoftposcurfucoa.m 
 |-  ( ph -> M = ( ( 1st ` .o. ) ` F ) )
6 prcoftposcurfucoa.f 
 |-  ( ph -> F e. ( C Func D ) )
7 relfunc 
 |-  Rel ( C Func D )
8 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
9 7 6 8 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
10 9 oveq2d 
 |-  ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
11 9 fveq2d 
 |-  ( ph -> ( ( 1st ` .o. ) ` F ) = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
12 5 11 eqtrd 
 |-  ( ph -> M = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
13 6 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
14 1 2 3 4 12 13 prcoftposcurfuco 
 |-  ( ph -> ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) = M )
15 10 14 eqtrd 
 |-  ( ph -> ( <. D , E >. -o.F F ) = M )