Theorem termccofix

Description: Post-composition by an object-fixing endofunctor leaves a functor with terminal source literally unchanged. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	termcfunc1eq.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcfunc1eq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	termccofix.s	$$⊢\phi \to S\in \left(D\mathrm{Func}D\right)$$
	termccofix.i	$$⊢\phi \to 1^{st}\left(S\right)={\mathrm{I}\upharpoonright }_A$$
Assertion	termccofix	$$⊢\phi \to S{\circ }_{\mathrm{func}}F=F$$

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcfunc1eq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		termccofix.s	$$⊢\phi \to S\in \left(D\mathrm{Func}D\right)$$
4		termccofix.i	$$⊢\phi \to 1^{st}\left(S\right)={\mathrm{I}\upharpoonright }_A$$
5	2 3	cofucl	$$⊢\phi \to S{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}D\right)$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7	1 6	termco	$$⊢\phi \to \bigcup {\mathrm{Base}}_C\in {\mathrm{Base}}_C$$
8	6 2 3 7	cofu1	$$⊢\phi \to 1^{st}\left(S{\circ }_{\mathrm{func}}F\right)\left(\bigcup {\mathrm{Base}}_C\right)=1^{st}\left(S\right)\left(1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\right)$$
9	4	fveq1d	$$⊢\phi \to 1^{st}\left(S\right)\left(1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\right)=\left({\mathrm{I}\upharpoonright }_A\right)\left(1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
11	2	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
12	6 10 11	funcf1	$$⊢\phi \to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
13	12 7	ffvelcdmd	$$⊢\phi \to 1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\in {\mathrm{Base}}_D$$
14	4	dmeqd	$$⊢\phi \to \mathrm{dom}{1}^{st}\left(S\right)=\mathrm{dom}\left({\mathrm{I}\upharpoonright }_A\right)$$
15		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_A\right)=A$$
16	14 15	eqtrdi	$$⊢\phi \to \mathrm{dom}{1}^{st}\left(S\right)=A$$
17	3	func1st2nd	$$⊢\phi \to 1^{st}\left(S\right)\left(D\mathrm{Func}D\right)2^{nd}\left(S\right)$$
18	10 10 17	funcf1	$$⊢\phi \to 1^{st}\left(S\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_D$$
19	18	fdmd	$$⊢\phi \to \mathrm{dom}{1}^{st}\left(S\right)={\mathrm{Base}}_D$$
20	16 19	eqtr3d	$$⊢\phi \to A={\mathrm{Base}}_D$$
21	13 20	eleqtrrd	$$⊢\phi \to 1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\in A$$
22		fvresi	$$⊢1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\right)=1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)$$
23	21 22	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right)\left(1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)\right)=1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)$$
24	8 9 23	3eqtrd	$$⊢\phi \to 1^{st}\left(S{\circ }_{\mathrm{func}}F\right)\left(\bigcup {\mathrm{Base}}_C\right)=1^{st}\left(F\right)\left(\bigcup {\mathrm{Base}}_C\right)$$
25	1 5 6 2 7 24	termcfunc1eq	$$⊢\phi \to S{\circ }_{\mathrm{func}}F=F$$