Theorem cofid1a

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$$
	cofid1a.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	cofid1a.g	$$⊢\phi \to G\in \left(E\mathrm{Func}D\right)$$
	cofid1a.o	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=I$$
Assertion	cofid1a	$$⊢\phi \to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\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		cofid1a.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
5		cofid1a.g	$$⊢\phi \to G\in \left(E\mathrm{Func}D\right)$$
6		cofid1a.o	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=I$$
7	6	fveq2d	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)=1^{st}\left(I\right)$$
8	7	fveq1d	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)\left(X\right)=1^{st}\left(I\right)\left(X\right)$$
9	2 4 5 3	cofu1	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)\left(X\right)=1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)$$
10	4	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
11	10	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
12	1 2 11 3	idfu1	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=X$$
13	8 9 12	3eqtr3d	$$⊢\phi \to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)=X$$