Theorem cofuswapfcl

Description: The bifunctor pre-composed with a swap functor is a bifunctor. (Contributed by Zhi Wang, 10-Oct-2025)

	Ref	Expression
Hypotheses	cofuswapf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	cofuswapf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	cofuswapf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
	cofuswapf1.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
Assertion	cofuswapfcl	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cofuswapf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		cofuswapf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		cofuswapf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
4		cofuswapf1.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
5		eqid	⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
6		eqid	⊢ ( 𝐷 ×c 𝐶 ) = ( 𝐷 ×c 𝐶 )
7	1 2 5 6	swapffunca	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func ( 𝐷 ×c 𝐶 ) ) )
8	7 3	cofucl	⊢ ( 𝜑 → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
9	4 8	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )