Theorem termcpostfix

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

	Ref	Expression
Hypotheses	termcfunc1eq.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcpostfix.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	termcpostfix.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐷 )
	termcpostfix.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curryF ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐷 ) )
	termcpostfix.k	⊢ 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 )
	termcpostfix.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐷 ) )
	termcpostfix.i	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) = ( I ↾ 𝐴 ) )
Assertion	termcpostfix	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝑄 Func 𝑄 ) ∧ ( 1st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcpostfix.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
3		termcpostfix.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐷 )
4		termcpostfix.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curryF ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐷 ) )
5		termcpostfix.k	⊢ 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 )
6		termcpostfix.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐷 ) )
7		termcpostfix.i	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) = ( I ↾ 𝐴 ) )
8	1	termccatd	⊢ ( 𝜑 → 𝐶 ∈ Cat )
9	2 3 4 6 8 5 2	postcofcl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
10	2 3 4 6 8 5	postcof1st	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐶 ∈ TermCat )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑔 ∈ ( 𝐶 Func 𝐷 ) )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐷 ) )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) = ( I ↾ 𝐴 ) )
15	11 12 13 14	termccofix	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( 𝐹 ∘func 𝑔 ) = 𝑔 )
16	15	mpteq2dva	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ 𝑔 ) )
17	10 16	eqtrd	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ 𝑔 ) )
18		mptresid	⊢ ( I ↾ ( 𝐶 Func 𝐷 ) ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ 𝑔 )
19	17 18	eqtr4di	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐷 ) ) )
20	9 19	jca	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝑄 Func 𝑄 ) ∧ ( 1st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐷 ) ) ) )