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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
	fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
	fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
	fucoaltne.n	⊢ ( 𝜑 → ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) ≠ 𝐴 )
Assertion	fucoaltne	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ≠ ( 2nd ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
2		fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
3		fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
5		fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
6		fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
7		fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
8		fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
9		fucoaltne.n	⊢ ( 𝜑 → ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) ≠ 𝐴 )
10		eqid	⊢ ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) ) = ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) )
11		eqid	⊢ ( idfunc ‘ 𝐶 ) = ( idfunc ‘ 𝐶 )
12		eqid	⊢ ( Id ‘ ( 𝐶 FuncCat 𝐶 ) ) = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	fucoaltnelem	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ≠ ( 2nd ‘ 𝐿 ) )