Metamath Proof Explorer

Theorem precoffunc

Description: The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025) (Proof shortened by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses precoffunc.r 
|- R = ( D FuncCat E )
precoffunc.b 
|- B = ( D Func E )
precoffunc.n 
|- N = ( D Nat E )
precoffunc.f 
|- ( ph -> F ( C Func D ) G )
precoffunc.e 
|- ( ph -> E e. Cat )
precoffunc.k 
|- ( ph -> K = ( g e. B |-> ( g o.func <. F , G >. ) ) )
precoffunc.l 
|- ( ph -> L = ( g e. B , h e. B |-> ( a e. ( g N h ) |-> ( a o. F ) ) ) )
precoffunc.s 
|- S = ( C FuncCat E )
Assertion precoffunc 
|- ( ph -> K ( R Func S ) L )

Proof

Step Hyp Ref Expression
1 precoffunc.r 
 |-  R = ( D FuncCat E )
2 precoffunc.b 
 |-  B = ( D Func E )
3 precoffunc.n 
 |-  N = ( D Nat E )
4 precoffunc.f 
 |-  ( ph -> F ( C Func D ) G )
5 precoffunc.e 
 |-  ( ph -> E e. Cat )
6 precoffunc.k 
 |-  ( ph -> K = ( g e. B |-> ( g o.func <. F , G >. ) ) )
7 precoffunc.l 
 |-  ( ph -> L = ( g e. B , h e. B |-> ( a e. ( g N h ) |-> ( a o. F ) ) ) )
8 precoffunc.s 
 |-  S = ( C FuncCat E )
9 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
10 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 ) ) ) )
11 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
12 4 11 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
13 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 >. ) )
14 1 2 3 4 5 6 7 9 10 13 precofval3 
 |-  ( ph -> <. K , L >. = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) )
15 9 1 10 12 5 14 8 precofcl 
 |-  ( ph -> <. K , L >. e. ( R Func S ) )
16 df-br 
 |-  ( K ( R Func S ) L <-> <. K , L >. e. ( R Func S ) )
17 15 16 sylibr 
 |-  ( ph -> K ( R Func S ) L )