Theorem fuco112x

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fuco11.f	|- ( ph -> F ( C Func D ) G )
	fuco11.k	|- ( ph -> K ( D Func E ) L )
	fuco11.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
	fuco111x.x	|- ( ph -> X e. ( Base ` C ) )
	fuco112x.y	|- ( ph -> Y e. ( Base ` C ) )
Assertion	fuco112x	|- ( ph -> ( X ( 2nd ` ( O ` U ) ) Y ) = ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2		fuco11.f	|- ( ph -> F ( C Func D ) G )
3		fuco11.k	|- ( ph -> K ( D Func E ) L )
4		fuco11.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5		fuco111x.x	|- ( ph -> X e. ( Base ` C ) )
6		fuco112x.y	|- ( ph -> Y e. ( Base ` C ) )
7		eqid	|- ( Base ` C ) = ( Base ` C )
8	1 2 3 4 7	fuco112	|- ( ph -> ( 2nd ` ( O ` U ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) )
9		simprl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
10	9	fveq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( F ` x ) = ( F ` X ) )
11		simprr	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
12	11	fveq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( F ` y ) = ( F ` Y ) )
13	10 12	oveq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( F ` x ) L ( F ` y ) ) = ( ( F ` X ) L ( F ` Y ) ) )
14	9 11	oveq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x G y ) = ( X G Y ) )
15	13 14	coeq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) = ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) )
16		ovexd	|- ( ph -> ( ( F ` X ) L ( F ` Y ) ) e. _V )
17		ovexd	|- ( ph -> ( X G Y ) e. _V )
18	16 17	coexd	|- ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) e. _V )
19	8 15 5 6 18	ovmpod	|- ( ph -> ( X ( 2nd ` ( O ` U ) ) Y ) = ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) )