Metamath Proof Explorer

Theorem fucoaltfunc

Description: Post-compose functor composition with an object-fixing endofunctor of its target. The original object function remains literally fixed for arbitrary source and intermediate categories. (Contributed by Zhi Wang, 14-Sep-2026)

		Ref	Expression
	Hypotheses	fucoaltfunc.q	$⊢ Q = C FuncCat E$
		fucoaltfunc.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
		fucoaltfunc.l	No typesetting found for \|- L = ( <. C , D >. o.F E ) with typecode \|-
		fucoaltfunc.c	$⊢ φ \to C \in Cat$
		fucoaltfunc.d	$⊢ φ \to D \in Cat$
		fucoaltfunc.e	$⊢ φ \to E \in Cat$
		fucoaltfunc.k	$⊢ φ \to K \in (Q Func Q)$
		fucoaltfunc.i	$⊢ φ \to 1^{st} (K) = {I ↾}_{(C Func E)}$
	Assertion	fucoaltfunc	$⊢ φ \to 1^{st} (L) (T Func Q) 2^{nd} (K \circ_{func} L)$

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	$⊢ Q = C FuncCat E$
2		fucoaltfunc.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
3		fucoaltfunc.l	Could not format L = ( <. C , D >. o.F E ) : No typesetting found for \|- L = ( <. C , D >. o.F E ) with typecode \|-
4		fucoaltfunc.c	$⊢ φ \to C \in Cat$
5		fucoaltfunc.d	$⊢ φ \to D \in Cat$
6		fucoaltfunc.e	$⊢ φ \to E \in Cat$
7		fucoaltfunc.k	$⊢ φ \to K \in (Q Func Q)$
8		fucoaltfunc.i	$⊢ φ \to 1^{st} (K) = {I ↾}_{(C Func E)}$
9	1	fucbas	$⊢ C Func E = {Base}_{Q}$
10	2 1 4 5 6	fucofunca	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) ) with typecode \|-
11	3 10	eqeltrid	$⊢ φ \to L \in (T Func Q)$
12	9 11 7 8	cofu1stfix	$⊢ φ \to 1^{st} (K \circ_{func} L) = 1^{st} (L)$
13	11 7	cofucl	$⊢ φ \to K \circ_{func} L \in (T Func Q)$
14	13	func1st2nd	$⊢ φ \to 1^{st} (K \circ_{func} L) (T Func Q) 2^{nd} (K \circ_{func} L)$
15	12 14	breq1dd	$⊢ φ \to 1^{st} (L) (T Func Q) 2^{nd} (K \circ_{func} L)$