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	|- ( ph -> C e. Cat )
	cofuswapf1.d	|- ( ph -> D e. Cat )
	cofuswapf1.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
	cofuswapf1.g	|- ( ph -> G = ( F o.func ( C swapF D ) ) )
Assertion	cofuswapfcl	|- ( ph -> G e. ( ( C Xc. D ) Func E ) )

Proof

Step	Hyp	Ref	Expression
1		cofuswapf1.c	|- ( ph -> C e. Cat )
2		cofuswapf1.d	|- ( ph -> D e. Cat )
3		cofuswapf1.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
4		cofuswapf1.g	|- ( ph -> G = ( F o.func ( C swapF D ) ) )
5		eqid	|- ( C Xc. D ) = ( C Xc. D )
6		eqid	|- ( D Xc. C ) = ( D Xc. C )
7	1 2 5 6	swapffunca	|- ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) )
8	7 3	cofucl	|- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
9	4 8	eqeltrd	|- ( ph -> G e. ( ( C Xc. D ) Func E ) )