Metamath Proof Explorer

Theorem precofval3

Description: Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed 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 ) ) ) )
precofval3.q 
|- Q = ( C FuncCat D )
precofval3.o 
|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
precofval3.m 
|- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) )
Assertion precofval3 
|- ( ph -> <. K , L >. = M )

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 precofval3.q 
 |-  Q = ( C FuncCat D )
9 precofval3.o 
 |-  ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
10 precofval3.m 
 |-  ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) )
11 2 mpteq1i 
 |-  ( g e. B |-> ( g o.func <. F , G >. ) ) = ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) )
12 6 11 eqtrdi 
 |-  ( ph -> K = ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) )
13 2 a1i 
 |-  ( ph -> B = ( D Func E ) )
14 3 a1i 
 |-  ( ph -> N = ( D Nat E ) )
15 14 oveqd 
 |-  ( ph -> ( g N h ) = ( g ( D Nat E ) h ) )
16 relfunc 
 |-  Rel ( C Func D )
17 brrelex12 
 |-  ( ( Rel ( C Func D ) /\ F ( C Func D ) G ) -> ( F e. _V /\ G e. _V ) )
18 16 4 17 sylancr 
 |-  ( ph -> ( F e. _V /\ G e. _V ) )
19 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
20 18 19 syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
21 20 eqcomd 
 |-  ( ph -> F = ( 1st ` <. F , G >. ) )
22 21 coeq2d 
 |-  ( ph -> ( a o. F ) = ( a o. ( 1st ` <. F , G >. ) ) )
23 15 22 mpteq12dv 
 |-  ( ph -> ( a e. ( g N h ) |-> ( a o. F ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) )
24 13 13 23 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 >. ) ) ) ) )
25 7 24 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 >. ) ) ) ) )
26 12 25 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 >. ) ) ) ) >. )
27 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
28 4 27 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
29 8 1 9 28 5 10 precofval2 
 |-  ( ph -> M = <. ( 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 >. ) ) ) ) >. )
30 26 29 eqtr4d 
 |-  ( ph -> <. K , L >. = M )