Metamath Proof Explorer

Theorem precofval2

Description: Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025)

Ref Expression
Hypotheses precofval.q 
|- Q = ( C FuncCat D )
precofval.r 
|- R = ( D FuncCat E )
precofval.o 
|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
precofval.f 
|- ( ph -> F e. ( C Func D ) )
precofval.e 
|- ( ph -> E e. Cat )
precofval.k 
|- ( ph -> K = ( ( 1st ` .o. ) ` F ) )
Assertion precofval2 
|- ( ph -> K = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` F ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 precofval.q 
 |-  Q = ( C FuncCat D )
2 precofval.r 
 |-  R = ( D FuncCat E )
3 precofval.o 
 |-  ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
4 precofval.f 
 |-  ( ph -> F e. ( C Func D ) )
5 precofval.e 
 |-  ( ph -> E e. Cat )
6 precofval.k 
 |-  ( ph -> K = ( ( 1st ` .o. ) ` F ) )
7 1 2 3 4 5 6 precofval 
 |-  ( ph -> K = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. )
8 eqid 
 |-  ( D Nat E ) = ( D Nat E )
9 id 
 |-  ( a e. ( g ( D Nat E ) h ) -> a e. ( g ( D Nat E ) h ) )
10 8 9 nat1st2nd 
 |-  ( a e. ( g ( D Nat E ) h ) -> a e. ( <. ( 1st ` g ) , ( 2nd ` g ) >. ( D Nat E ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 8 10 11 natfn 
 |-  ( a e. ( g ( D Nat E ) h ) -> a Fn ( Base ` D ) )
13 dffn2 
 |-  ( a Fn ( Base ` D ) <-> a : ( Base ` D ) --> _V )
14 12 13 sylib 
 |-  ( a e. ( g ( D Nat E ) h ) -> a : ( Base ` D ) --> _V )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 relfunc 
 |-  Rel ( C Func D )
17 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
18 16 4 17 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
19 15 11 18 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
20 fcompt 
 |-  ( ( a : ( Base ` D ) --> _V /\ ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) ) -> ( a o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) )
21 14 19 20 syl2anr 
 |-  ( ( ph /\ a e. ( g ( D Nat E ) h ) ) -> ( a o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) )
22 21 mpteq2dva 
 |-  ( ph -> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) )
23 22 mpoeq3dv 
 |-  ( ph -> ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` F ) ) ) ) = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) )
24 23 opeq2d 
 |-  ( ph -> <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` F ) ) ) ) >. = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. )
25 7 24 eqtr4d 
 |-  ( ph -> K = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` F ) ) ) ) >. )