Theorem fuco2

Description: The morphism part of the functor composition bifunctor. (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 )
	fuco1.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fuco1.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
Assertion	fuco2	|- ( ph -> P = ( 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		fuco1.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
5		fuco1.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
6	1 2 3 4 5	fucofval	|- ( ph -> <. O , P >. = <. ( 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 ) ) ) ) ) ) >. )
7	1 2 3 4	fucoelvv	|- ( ph -> <. O , P >. e. ( _V X. _V ) )
8		opelxp1	|- ( <. O , P >. e. ( _V X. _V ) -> O e. _V )
9	7 8	syl	|- ( ph -> O e. _V )
10		opelxp2	|- ( <. O , P >. e. ( _V X. _V ) -> P e. _V )
11	7 10	syl	|- ( ph -> P e. _V )
12		opthg	|- ( ( O e. _V /\ P e. _V ) -> ( <. O , P >. = <. ( 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 ) ) ) ) ) ) >. <-> ( O = ( o.func |` W ) /\ P = ( 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 ) ) ) ) ) ) ) ) )
13	9 11 12	syl2anc	|- ( ph -> ( <. O , P >. = <. ( 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 ) ) ) ) ) ) >. <-> ( O = ( o.func |` W ) /\ P = ( 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 ) ) ) ) ) ) ) ) )
14	6 13	mpbid	|- ( ph -> ( O = ( o.func |` W ) /\ P = ( 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 ) ) ) ) ) ) ) )
15	14	simprd	|- ( ph -> P = ( 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 ) ) ) ) ) ) )