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	$$⊢\phi \to C\in \mathrm{Cat}$$
	cofuswapf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	cofuswapf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	cofuswapf1.g	No typesetting found for |- ( ph -> G = ( F o.func ( C swapF D ) ) ) with typecode |-
Assertion	cofuswapfcl	$$⊢\phi \to G\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofuswapf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		cofuswapf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
3		cofuswapf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
4		cofuswapf1.g	Could not format ( ph -> G = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ph -> G = ( F o.func ( C swapF D ) ) ) with typecode |-
5		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
6		eqid	$$⊢D{\times }_{c}C=D{\times }_{c}C$$
7	1 2 5 6	swapffunca	Could not format ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) ) with typecode |-
8	7 3	cofucl	Could not format ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) with typecode |-
9	4 8	eqeltrd	$$⊢\phi \to G\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$