Theorem fuco11idx

Description: The identity morphism of the mapped object. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
	fuco11.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	fuco11.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
	fuco11.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
	fuco11id.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fuco11id.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
	fuco11id.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(E\right)$$
	fuco11idx.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
Assertion	fuco11idx	$$⊢\phi \to I\left(O\left(U\right)\right)\left(X\right)=\underset{\dot{}}{1}\left(K\left(F\left(X\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
2		fuco11.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
3		fuco11.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
4		fuco11.u	$$⊢\phi \to U=⟨⟨K,L⟩,⟨F,G⟩⟩$$
5		fuco11id.q	$$⊢Q=C\mathrm{FuncCat}E$$
6		fuco11id.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
7		fuco11id.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(E\right)$$
8		fuco11idx.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
9	1 2 3 4 5 6 7	fuco11id	$$⊢\phi \to I\left(O\left(U\right)\right)=\underset{\dot{}}{1}\circ \left(K\circ F\right)$$
10		coass	$$⊢\left(\underset{\dot{}}{1}\circ K\right)\circ F=\underset{\dot{}}{1}\circ \left(K\circ F\right)$$
11	9 10	eqtr4di	$$⊢\phi \to I\left(O\left(U\right)\right)=\left(\underset{\dot{}}{1}\circ K\right)\circ F$$
12	11	fveq1d	$$⊢\phi \to I\left(O\left(U\right)\right)\left(X\right)=\left(\left(\underset{\dot{}}{1}\circ K\right)\circ F\right)\left(X\right)$$
13		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
14		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
15	13 14 2	funcf1	$$⊢\phi \to F:{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
16	15 8	fvco3d	$$⊢\phi \to \left(\left(\underset{\dot{}}{1}\circ K\right)\circ F\right)\left(X\right)=\left(\underset{\dot{}}{1}\circ K\right)\left(F\left(X\right)\right)$$
17		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
18	14 17 3	funcf1	$$⊢\phi \to K:{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
19	15 8	ffvelcdmd	$$⊢\phi \to F\left(X\right)\in {\mathrm{Base}}_D$$
20	18 19	fvco3d	$$⊢\phi \to \left(\underset{\dot{}}{1}\circ K\right)\left(F\left(X\right)\right)=\underset{\dot{}}{1}\left(K\left(F\left(X\right)\right)\right)$$
21	12 16 20	3eqtrd	$$⊢\phi \to I\left(O\left(U\right)\right)\left(X\right)=\underset{\dot{}}{1}\left(K\left(F\left(X\right)\right)\right)$$