Theorem fuco11id

Description: The identity morphism of the mapped object. (Contributed by Zhi Wang, 30-Sep-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)$$
Assertion	fuco11id	$$⊢\phi \to I\left(O\left(U\right)\right)=\underset{\dot{}}{1}\circ \left(K\circ F\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	1 2 3 4	fuco11cl	$$⊢\phi \to O\left(U\right)\in \left(C\mathrm{Func}E\right)$$
9	5 6 7 8	fucid	$$⊢\phi \to I\left(O\left(U\right)\right)=\underset{\dot{}}{1}\circ 1^{st}\left(O\left(U\right)\right)$$
10	1 2 3 4	fuco111	$$⊢\phi \to 1^{st}\left(O\left(U\right)\right)=K\circ F$$
11	10	coeq2d	$$⊢\phi \to \underset{\dot{}}{1}\circ 1^{st}\left(O\left(U\right)\right)=\underset{\dot{}}{1}\circ \left(K\circ F\right)$$
12	9 11	eqtrd	$$⊢\phi \to I\left(O\left(U\right)\right)=\underset{\dot{}}{1}\circ \left(K\circ F\right)$$