Theorem cofu1stfix

Description: Post-composition by an object-fixing functor preserves the entire object function, including its exact domain. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	cofu1stfix.a	$$⊢A={\mathrm{Base}}_E$$
	cofu1stfix.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	cofu1stfix.k	$$⊢\phi \to K\in \left(E\mathrm{Func}E\right)$$
	cofu1stfix.i	$$⊢\phi \to 1^{st}\left(K\right)={\mathrm{I}\upharpoonright }_A$$
Assertion	cofu1stfix	$$⊢\phi \to 1^{st}\left(K{\circ }_{\mathrm{func}}F\right)=1^{st}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofu1stfix.a	$$⊢A={\mathrm{Base}}_E$$
2		cofu1stfix.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
3		cofu1stfix.k	$$⊢\phi \to K\in \left(E\mathrm{Func}E\right)$$
4		cofu1stfix.i	$$⊢\phi \to 1^{st}\left(K\right)={\mathrm{I}\upharpoonright }_A$$
5		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
6	5 2 3	cofu1st	$$⊢\phi \to 1^{st}\left(K{\circ }_{\mathrm{func}}F\right)=1^{st}\left(K\right)\circ 1^{st}\left(F\right)$$
7	4	coeq1d	$$⊢\phi \to 1^{st}\left(K\right)\circ 1^{st}\left(F\right)=\left({\mathrm{I}\upharpoonright }_A\right)\circ 1^{st}\left(F\right)$$
8	2	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
9	5 1 8	funcf1	$$⊢\phi \to 1^{st}\left(F\right):{\mathrm{Base}}_D⟶A$$
10		fcoi2	$$⊢1^{st}\left(F\right):{\mathrm{Base}}_D⟶A\to \left({\mathrm{I}\upharpoonright }_A\right)\circ 1^{st}\left(F\right)=1^{st}\left(F\right)$$
11	9 10	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right)\circ 1^{st}\left(F\right)=1^{st}\left(F\right)$$
12	6 7 11	3eqtrd	$$⊢\phi \to 1^{st}\left(K{\circ }_{\mathrm{func}}F\right)=1^{st}\left(F\right)$$