Metamath Proof Explorer

Theorem fucoaltne

Description: A changed natural transformation witnesses that post-composed functor composition has a different morphism part. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

		Ref	Expression
	Hypotheses	fucoaltfunc.q	$⊢ Q = C FuncCat E$
		fucoaltval.l	No typesetting found for \|- L = ( <. C , C >. o.F E ) with typecode \|-
		fucoaltval.c	$⊢ φ \to C \in Cat$
		fucoaltval.e	$⊢ φ \to E \in Cat$
		fucoaltval.k	$⊢ φ \to K \in (Q Func Q)$
		fucoaltval.f	$⊢ φ \to F \in (C Func E)$
		fucoaltval.g	$⊢ φ \to G \in (C Func E)$
		fucoaltval.a	$⊢ φ \to A \in (F (C Nat E) G)$
		fucoaltne.n	$⊢ φ \to (F 2^{nd} (K) G) (A) \neq A$
	Assertion	fucoaltne	$⊢ φ \to 2^{nd} (K \circ_{func} L) \neq 2^{nd} (L)$

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	$⊢ Q = C FuncCat E$
2		fucoaltval.l	Could not format L = ( <. C , C >. o.F E ) : No typesetting found for \|- L = ( <. C , C >. o.F E ) with typecode \|-
3		fucoaltval.c	$⊢ φ \to C \in Cat$
4		fucoaltval.e	$⊢ φ \to E \in Cat$
5		fucoaltval.k	$⊢ φ \to K \in (Q Func Q)$
6		fucoaltval.f	$⊢ φ \to F \in (C Func E)$
7		fucoaltval.g	$⊢ φ \to G \in (C Func E)$
8		fucoaltval.a	$⊢ φ \to A \in (F (C Nat E) G)$
9		fucoaltne.n	$⊢ φ \to (F 2^{nd} (K) G) (A) \neq A$
10		eqid	$⊢ (C FuncCat E) \times_{c} (C FuncCat C) = (C FuncCat E) \times_{c} (C FuncCat C)$
11		eqid	$⊢ {id}_{func} (C) = {id}_{func} (C)$
12		eqid	$⊢ Id (C FuncCat C) = Id (C FuncCat C)$
13	1 2 3 4 5 6 7 8 9 10 11 12	fucoaltnelem	$⊢ φ \to 2^{nd} (K \circ_{func} L) \neq 2^{nd} (L)$