Theorem fuco11cl

Description: The object part of the functor composition bifunctor maps into ( C Func E ) . (Contributed by Zhi Wang, 30-Sep-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 >. >. )
Assertion	fuco11cl	|- ( ph -> ( O ` U ) e. ( C Func E ) )

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	2	funcrcl2	|- ( ph -> C e. Cat )
6	3	funcrcl2	|- ( ph -> D e. Cat )
7	3	funcrcl3	|- ( ph -> E e. Cat )
8		eqidd	|- ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
9	5 6 7 1 8	fucof1	|- ( ph -> O : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
10	8 4 3 2	fuco2eld	|- ( ph -> U e. ( ( D Func E ) X. ( C Func D ) ) )
11	9 10	ffvelcdmd	|- ( ph -> ( O ` U ) e. ( C Func E ) )