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	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcfunc1eq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	termccofix.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐷 Func 𝐷 ) )
	termccofix.i	⊢ ( 𝜑 → ( 1st ‘ 𝑆 ) = ( I ↾ 𝐴 ) )
Assertion	termccofix	⊢ ( 𝜑 → ( 𝑆 ∘func 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcfunc1eq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		termccofix.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐷 Func 𝐷 ) )
4		termccofix.i	⊢ ( 𝜑 → ( 1st ‘ 𝑆 ) = ( I ↾ 𝐴 ) )
5	2 3	cofucl	⊢ ( 𝜑 → ( 𝑆 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐷 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7	1 6	termco	⊢ ( 𝜑 → ∪ ( Base ‘ 𝐶 ) ∈ ( Base ‘ 𝐶 ) )
8	6 2 3 7	cofu1	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑆 ∘func 𝐹 ) ) ‘ ∪ ( Base ‘ 𝐶 ) ) = ( ( 1st ‘ 𝑆 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ) )
9	4	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ 𝑆 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ) = ( ( I ↾ 𝐴 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ) )
10		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11	2	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
12	6 10 11	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
13	12 7	ffvelcdmd	⊢ ( 𝜑 → ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ∈ ( Base ‘ 𝐷 ) )
14	4	dmeqd	⊢ ( 𝜑 → dom ( 1st ‘ 𝑆 ) = dom ( I ↾ 𝐴 ) )
15		dmresi	⊢ dom ( I ↾ 𝐴 ) = 𝐴
16	14 15	eqtrdi	⊢ ( 𝜑 → dom ( 1st ‘ 𝑆 ) = 𝐴 )
17	3	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝑆 ) ( 𝐷 Func 𝐷 ) ( 2nd ‘ 𝑆 ) )
18	10 10 17	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝑆 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐷 ) )
19	18	fdmd	⊢ ( 𝜑 → dom ( 1st ‘ 𝑆 ) = ( Base ‘ 𝐷 ) )
20	16 19	eqtr3d	⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝐷 ) )
21	13 20	eleqtrrd	⊢ ( 𝜑 → ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ∈ 𝐴 )
22		fvresi	⊢ ( ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ) = ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) )
23	21 22	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) ) = ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) )
24	8 9 23	3eqtrd	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑆 ∘func 𝐹 ) ) ‘ ∪ ( Base ‘ 𝐶 ) ) = ( ( 1st ‘ 𝐹 ) ‘ ∪ ( Base ‘ 𝐶 ) ) )
25	1 5 6 2 7 24	termcfunc1eq	⊢ ( 𝜑 → ( 𝑆 ∘func 𝐹 ) = 𝐹 )