Metamath Proof Explorer

Theorem fucofval

Description: Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant ( fucofvalne ). (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses fucofval.c 
|- ( ph -> C e. T )
fucofval.d 
|- ( ph -> D e. U )
fucofval.e 
|- ( ph -> E e. V )
fucofval.o 
|- ( ph -> ( <. C , D >. o.F E ) = .o. )
fucofval.w 
|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
Assertion fucofval 
|- ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 fucofval.c 
 |-  ( ph -> C e. T )
2 fucofval.d 
 |-  ( ph -> D e. U )
3 fucofval.e 
 |-  ( ph -> E e. V )
4 fucofval.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = .o. )
5 fucofval.w 
 |-  ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
6 opex 
 |-  <. C , D >. e. _V
7 6 a1i 
 |-  ( ph -> <. C , D >. e. _V )
8 op1stg 
 |-  ( ( C e. T /\ D e. U ) -> ( 1st ` <. C , D >. ) = C )
9 1 2 8 syl2anc 
 |-  ( ph -> ( 1st ` <. C , D >. ) = C )
10 op2ndg 
 |-  ( ( C e. T /\ D e. U ) -> ( 2nd ` <. C , D >. ) = D )
11 1 2 10 syl2anc 
 |-  ( ph -> ( 2nd ` <. C , D >. ) = D )
12 7 9 11 3 4 5 fucofvalg 
 |-  ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )