Theorem fuco11idx

Description: The identity morphism of the mapped object. (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 >. >. )
	fuco11id.q	|- Q = ( C FuncCat E )
	fuco11id.i	|- I = ( Id ` Q )
	fuco11id.1	|- .1. = ( Id ` E )
	fuco11idx.x	|- ( ph -> X e. ( Base ` C ) )
Assertion	fuco11idx	|- ( ph -> ( ( I ` ( O ` U ) ) ` X ) = ( .1. ` ( K ` ( F ` X ) ) ) )

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		fuco11id.q	|- Q = ( C FuncCat E )
6		fuco11id.i	|- I = ( Id ` Q )
7		fuco11id.1	|- .1. = ( Id ` E )
8		fuco11idx.x	|- ( ph -> X e. ( Base ` C ) )
9	1 2 3 4 5 6 7	fuco11id	|- ( ph -> ( I ` ( O ` U ) ) = ( .1. o. ( K o. F ) ) )
10		coass	|- ( ( .1. o. K ) o. F ) = ( .1. o. ( K o. F ) )
11	9 10	eqtr4di	|- ( ph -> ( I ` ( O ` U ) ) = ( ( .1. o. K ) o. F ) )
12	11	fveq1d	|- ( ph -> ( ( I ` ( O ` U ) ) ` X ) = ( ( ( .1. o. K ) o. F ) ` X ) )
13		eqid	|- ( Base ` C ) = ( Base ` C )
14		eqid	|- ( Base ` D ) = ( Base ` D )
15	13 14 2	funcf1	|- ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
16	15 8	fvco3d	|- ( ph -> ( ( ( .1. o. K ) o. F ) ` X ) = ( ( .1. o. K ) ` ( F ` X ) ) )
17		eqid	|- ( Base ` E ) = ( Base ` E )
18	14 17 3	funcf1	|- ( ph -> K : ( Base ` D ) --> ( Base ` E ) )
19	15 8	ffvelcdmd	|- ( ph -> ( F ` X ) e. ( Base ` D ) )
20	18 19	fvco3d	|- ( ph -> ( ( .1. o. K ) ` ( F ` X ) ) = ( .1. ` ( K ` ( F ` X ) ) ) )
21	12 16 20	3eqtrd	|- ( ph -> ( ( I ` ( O ` U ) ) ` X ) = ( .1. ` ( K ` ( F ` X ) ) ) )