Theorem fuco11id

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

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	1 2 3 4	fuco11cl	|- ( ph -> ( O ` U ) e. ( C Func E ) )
9	5 6 7 8	fucid	|- ( ph -> ( I ` ( O ` U ) ) = ( .1. o. ( 1st ` ( O ` U ) ) ) )
10	1 2 3 4	fuco111	|- ( ph -> ( 1st ` ( O ` U ) ) = ( K o. F ) )
11	10	coeq2d	|- ( ph -> ( .1. o. ( 1st ` ( O ` U ) ) ) = ( .1. o. ( K o. F ) ) )
12	9 11	eqtrd	|- ( ph -> ( I ` ( O ` U ) ) = ( .1. o. ( K o. F ) ) )