Metamath Proof Explorer

Theorem prcoffunc

Description: The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025)

Ref Expression
Hypotheses prcoffunc.r 
|- R = ( D FuncCat E )
prcoffunc.e 
|- ( ph -> E e. Cat )
prcoffunc.s 
|- S = ( C FuncCat E )
prcoffunc.f 
|- ( ph -> F ( C Func D ) G )
Assertion prcoffunc 
|- ( ph -> ( <. D , E >. -o.F <. F , G >. ) e. ( R Func S ) )

Proof

Step Hyp Ref Expression
1 prcoffunc.r 
 |-  R = ( D FuncCat E )
2 prcoffunc.e 
 |-  ( ph -> E e. Cat )
3 prcoffunc.s 
 |-  S = ( C FuncCat E )
4 prcoffunc.f 
 |-  ( ph -> F ( C Func D ) G )
5 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
6 eqidd 
 |-  ( ph -> ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) = ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) )
7 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
8 4 7 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
9 eqidd 
 |-  ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) )
10 1 2 5 6 9 4 prcoftposcurfuco 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) )
11 5 1 6 8 2 10 3 precofcl 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) e. ( R Func S ) )