Theorem cofid1

Description: Express the object part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofid1a.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
	cofid1a.b	$$⊢B={\mathrm{Base}}_D$$
	cofid1a.x	$$⊢\phi \to X\in B$$
	cofid1.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	cofid1.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
	cofid1.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
Assertion	cofid1	$$⊢\phi \to K\left(F\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
2		cofid1a.b	$$⊢B={\mathrm{Base}}_D$$
3		cofid1a.x	$$⊢\phi \to X\in B$$
4		cofid1.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
5		cofid1.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
6		cofid1.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
7	5	func1st	$$⊢\phi \to 1^{st}\left(⟨K,L⟩\right)=K$$
8	4	func1st	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
9	8	fveq1d	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)\left(X\right)=F\left(X\right)$$
10	7 9	fveq12d	$$⊢\phi \to 1^{st}\left(⟨K,L⟩\right)\left(1^{st}\left(⟨F,G⟩\right)\left(X\right)\right)=K\left(F\left(X\right)\right)$$
11		df-br	$$⊢F\left(D\mathrm{Func}E\right)G\leftrightarrow ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
12	4 11	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
13		df-br	$$⊢K\left(E\mathrm{Func}D\right)L\leftrightarrow ⟨K,L⟩\in \left(E\mathrm{Func}D\right)$$
14	5 13	sylib	$$⊢\phi \to ⟨K,L⟩\in \left(E\mathrm{Func}D\right)$$
15	1 2 3 12 14 6	cofid1a	$$⊢\phi \to 1^{st}\left(⟨K,L⟩\right)\left(1^{st}\left(⟨F,G⟩\right)\left(X\right)\right)=X$$
16	10 15	eqtr3d	$$⊢\phi \to K\left(F\left(X\right)\right)=X$$