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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoaltfunc.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
	fucoaltfunc.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 )
	fucoaltfunc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoaltfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	fucoaltfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoaltfunc.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
	fucoaltfunc.i	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐸 ) ) )
Assertion	fucoaltfunc	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
2		fucoaltfunc.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
3		fucoaltfunc.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 )
4		fucoaltfunc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		fucoaltfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		fucoaltfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
7		fucoaltfunc.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
8		fucoaltfunc.i	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐸 ) ) )
9	1	fucbas	⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑄 )
10	2 1 4 5 6	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( 𝑇 Func 𝑄 ) )
11	3 10	eqeltrid	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑇 Func 𝑄 ) )
12	9 11 7 8	cofu1stfix	⊢ ( 𝜑 → ( 1st ‘ ( 𝐾 ∘func 𝐿 ) ) = ( 1st ‘ 𝐿 ) )
13	11 7	cofucl	⊢ ( 𝜑 → ( 𝐾 ∘func 𝐿 ) ∈ ( 𝑇 Func 𝑄 ) )
14	13	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ ( 𝐾 ∘func 𝐿 ) ) ( 𝑇 Func 𝑄 ) ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) )
15	12 14	breq1dd	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) )