Theorem fucofunca

Description: The functor composition bifunctor is a functor. See also fucofunc . (Contributed by Zhi Wang, 10-Oct-2025)

	Ref	Expression
Hypotheses	fucofunca.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
	fucofunca.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucofunca.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucofunca.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	fucofunca.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
Assertion	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( 𝑇 Func 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		fucofunca.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
2		fucofunca.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
3		fucofunca.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		fucofunca.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		fucofunca.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
6		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
7	3 4 5 6	fucoelvv	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) )
8		1st2nd2	⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
9	7 8	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
10	1 2 9 3 4 5	fucofunc	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ( 𝑇 Func 𝑄 ) ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) )
11		df-br	⊢ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ( 𝑇 Func 𝑄 ) ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ↔ ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ ∈ ( 𝑇 Func 𝑄 ) )
12	10 11	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ ∈ ( 𝑇 Func 𝑄 ) )
13	9 12	eqeltrd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( 𝑇 Func 𝑄 ) )