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	No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
	termcpostfix.q	$⊢ Q = C FuncCat D$
	termcpostfix.r	$⊢ R = D FuncCat D$
	termcpostfix.o	No typesetting found for \|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F D ) ) with typecode \|-
	termcpostfix.k	No typesetting found for \|- K = ( ( 1st ` .o. ) ` F ) with typecode \|-
	termcpostfix.f	$⊢ φ \to F \in (D Func D)$
	termcpostfix.i	$⊢ φ \to 1^{st} (F) = {I ↾}_{A}$
Assertion	termcpostfix	$⊢ φ \to (K \in (Q Func Q) \land 1^{st} (K) = {I ↾}_{(C Func D)})$

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		termcpostfix.q	$⊢ Q = C FuncCat D$
3		termcpostfix.r	$⊢ R = D FuncCat D$
4		termcpostfix.o	Could not format .o. = ( <. R , Q >. curryF ( <. C , D >. o.F D ) ) : No typesetting found for \|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F D ) ) with typecode \|-
5		termcpostfix.k	Could not format K = ( ( 1st ` .o. ) ` F ) : No typesetting found for \|- K = ( ( 1st ` .o. ) ` F ) with typecode \|-
6		termcpostfix.f	$⊢ φ \to F \in (D Func D)$
7		termcpostfix.i	$⊢ φ \to 1^{st} (F) = {I ↾}_{A}$
8	1	termccatd	$⊢ φ \to C \in Cat$
9	2 3 4 6 8 5 2	postcofcl	$⊢ φ \to K \in (Q Func Q)$
10	2 3 4 6 8 5	postcof1st	$⊢ φ \to 1^{st} (K) = (g \in (C Func D) ⟼ F \circ_{func} g)$
11	1	adantr	Could not format ( ( ph /\ g e. ( C Func D ) ) -> C e. TermCat ) : No typesetting found for \|- ( ( ph /\ g e. ( C Func D ) ) -> C e. TermCat ) with typecode \|-
12		simpr	$⊢ (φ \land g \in (C Func D)) \to g \in (C Func D)$
13	6	adantr	$⊢ (φ \land g \in (C Func D)) \to F \in (D Func D)$
14	7	adantr	$⊢ (φ \land g \in (C Func D)) \to 1^{st} (F) = {I ↾}_{A}$
15	11 12 13 14	termccofix	$⊢ (φ \land g \in (C Func D)) \to F \circ_{func} g = g$
16	15	mpteq2dva	$⊢ φ \to (g \in (C Func D) ⟼ F \circ_{func} g) = (g \in (C Func D) ⟼ g)$
17	10 16	eqtrd	$⊢ φ \to 1^{st} (K) = (g \in (C Func D) ⟼ g)$
18		mptresid	$⊢ {I ↾}_{(C Func D)} = (g \in (C Func D) ⟼ g)$
19	17 18	eqtr4di	$⊢ φ \to 1^{st} (K) = {I ↾}_{(C Func D)}$
20	9 19	jca	$⊢ φ \to (K \in (Q Func Q) \land 1^{st} (K) = {I ↾}_{(C Func D)})$

Metamath Proof Explorer

Theorem termcpostfix

Proof