Metamath Proof Explorer

Theorem precoffunc

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

Ref Expression
Hypotheses precoffunc.r 
|- R = ( D FuncCat E )
precoffunc.s 
|- S = ( C 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 ) ) ) )
Assertion precoffunc 
|- ( ph -> K ( R Func S ) L )

Proof

Step Hyp Ref Expression
1 precoffunc.r 
 |-  R = ( D FuncCat E )
2 precoffunc.s 
 |-  S = ( C FuncCat E )
3 precoffunc.b 
 |-  B = ( D Func E )
4 precoffunc.n 
 |-  N = ( D Nat E )
5 precoffunc.f 
 |-  ( ph -> F ( C Func D ) G )
6 precoffunc.e 
 |-  ( ph -> E e. Cat )
7 precoffunc.k 
 |-  ( ph -> K = ( g e. B |-> ( g o.func <. F , G >. ) ) )
8 precoffunc.l 
 |-  ( ph -> L = ( g e. B , h e. B |-> ( a e. ( g N h ) |-> ( a o. F ) ) ) )
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 5 11 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
13 3 mpteq1i 
 |-  ( g e. B |-> ( g o.func <. F , G >. ) ) = ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) )
14 7 13 eqtrdi 
 |-  ( ph -> K = ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) )
15 3 a1i 
 |-  ( ph -> B = ( D Func E ) )
16 4 a1i 
 |-  ( ph -> N = ( D Nat E ) )
17 16 oveqd 
 |-  ( ph -> ( g N h ) = ( g ( D Nat E ) h ) )
18 relfunc 
 |-  Rel ( C Func D )
19 brrelex12 
 |-  ( ( Rel ( C Func D ) /\ F ( C Func D ) G ) -> ( F e. _V /\ G e. _V ) )
20 18 5 19 sylancr 
 |-  ( ph -> ( F e. _V /\ G e. _V ) )
21 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
22 20 21 syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
23 22 eqcomd 
 |-  ( ph -> F = ( 1st ` <. F , G >. ) )
24 23 coeq2d 
 |-  ( ph -> ( a o. F ) = ( a o. ( 1st ` <. F , G >. ) ) )
25 17 24 mpteq12dv 
 |-  ( ph -> ( a e. ( g N h ) |-> ( a o. F ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) )
26 15 15 25 mpoeq123dv 
 |-  ( ph -> ( g e. B , h e. B |-> ( a e. ( g N h ) |-> ( a o. F ) ) ) = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) )
27 8 26 eqtrd 
 |-  ( ph -> L = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) )
28 14 27 opeq12d 
 |-  ( ph -> <. K , L >. = <. ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. )
29 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 >. ) )
30 9 1 10 12 6 29 precofval2 
 |-  ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) = <. ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. )
31 28 30 eqtr4d 
 |-  ( ph -> <. K , L >. = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) )
32 9 1 10 12 6 31 2 precofcl 
 |-  ( ph -> <. K , L >. e. ( R Func S ) )
33 df-br 
 |-  ( K ( R Func S ) L <-> <. K , L >. e. ( R Func S ) )
34 32 33 sylibr 
 |-  ( ph -> K ( R Func S ) L )