Theorem cofuswapf2

Description: The morphism part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-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 |-
	cofuswapf1.a	$$⊢A={\mathrm{Base}}_C$$
	cofuswapf1.b	$$⊢B={\mathrm{Base}}_D$$
	cofuswapf1.x	$$⊢\phi \to X\in A$$
	cofuswapf1.y	$$⊢\phi \to Y\in B$$
	cofuswapf2.z	$$⊢\phi \to Z\in A$$
	cofuswapf2.w	$$⊢\phi \to W\in B$$
	cofuswapf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	cofuswapf2.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	cofuswapf2.m	$$⊢\phi \to M\in \left(XHZ\right)$$
	cofuswapf2.n	$$⊢\phi \to N\in \left(YJW\right)$$
Assertion	cofuswapf2	$$⊢\phi \to M\left(⟨X,Y⟩2^{nd}\left(G\right)⟨Z,W⟩\right)N=N\left(⟨Y,X⟩2^{nd}\left(F\right)⟨W,Z⟩\right)M$$

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		cofuswapf1.a	$$⊢A={\mathrm{Base}}_C$$
6		cofuswapf1.b	$$⊢B={\mathrm{Base}}_D$$
7		cofuswapf1.x	$$⊢\phi \to X\in A$$
8		cofuswapf1.y	$$⊢\phi \to Y\in B$$
9		cofuswapf2.z	$$⊢\phi \to Z\in A$$
10		cofuswapf2.w	$$⊢\phi \to W\in B$$
11		cofuswapf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
12		cofuswapf2.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
13		cofuswapf2.m	$$⊢\phi \to M\in \left(XHZ\right)$$
14		cofuswapf2.n	$$⊢\phi \to N\in \left(YJW\right)$$
15	4	fveq2d	Could not format ( ph -> ( 2nd ` G ) = ( 2nd ` ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` G ) = ( 2nd ` ( F o.func ( C swapF D ) ) ) ) with typecode |-
16	15	oveqd	Could not format ( ph -> ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) = ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ) : No typesetting found for |- ( ph -> ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) = ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ) with typecode |-
17	16	oveqd	Could not format ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) ) : No typesetting found for |- ( ph -> ( M ( <. X , Y >. ( 2nd ` G ) <. Z , W >. ) N ) = ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) ) with typecode |-
18		df-ov	Could not format ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. ) : No typesetting found for |- ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. ) with typecode |-
19		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
20	19 5 6	xpcbas	$$⊢A\times B={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
21		eqid	$$⊢D{\times }_{c}C=D{\times }_{c}C$$
22	1 2 19 21	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 |-
23	7 8	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(A\times B\right)$$
24	9 10	opelxpd	$$⊢\phi \to ⟨Z,W⟩\in \left(A\times B\right)$$
25		eqid	$$⊢\mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
26	13 14	opelxpd	$$⊢\phi \to ⟨M,N⟩\in \left(\left(XHZ\right)\times \left(YJW\right)\right)$$
27	19 5 6 11 12 7 8 9 10 25	xpchom2	$$⊢\phi \to ⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Z,W⟩=\left(XHZ\right)\times \left(YJW\right)$$
28	26 27	eleqtrrd	$$⊢\phi \to ⟨M,N⟩\in \left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Z,W⟩\right)$$
29	20 22 3 23 24 25 28	cofu2	Could not format ( ph -> ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) ) : No typesetting found for |- ( ph -> ( ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) ` <. M , N >. ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) ) with typecode |-
30	18 29	eqtrid	Could not format ( ph -> ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) ) : No typesetting found for |- ( ph -> ( M ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Z , W >. ) N ) = ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) ) with typecode |-
31		df-ov	Could not format ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) : No typesetting found for |- ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) with typecode |-
32	1 2	swapfelvv	Could not format ( ph -> ( C swapF D ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( _V X. _V ) ) with typecode |-
33		1st2nd2	Could not format ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
34	32 33	syl	Could not format ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
35	7 5	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
36	8 6	eleqtrdi	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
37	34 35 36	swapf1	Could not format ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. ) : No typesetting found for |- ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. ) with typecode |-
38	31 37	eqtr3id	Could not format ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. ) : No typesetting found for |- ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. ) with typecode |-
39		df-ov	Could not format ( Z ( 1st ` ( C swapF D ) ) W ) = ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) : No typesetting found for |- ( Z ( 1st ` ( C swapF D ) ) W ) = ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) with typecode |-
40	9 5	eleqtrdi	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
41	10 6	eleqtrdi	$$⊢\phi \to W\in {\mathrm{Base}}_D$$
42	34 40 41	swapf1	Could not format ( ph -> ( Z ( 1st ` ( C swapF D ) ) W ) = <. W , Z >. ) : No typesetting found for |- ( ph -> ( Z ( 1st ` ( C swapF D ) ) W ) = <. W , Z >. ) with typecode |-
43	39 42	eqtr3id	Could not format ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) = <. W , Z >. ) : No typesetting found for |- ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) = <. W , Z >. ) with typecode |-
44	38 43	oveq12d	Could not format ( ph -> ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) = ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ) : No typesetting found for |- ( ph -> ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) = ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ) with typecode |-
45		df-ov	Could not format ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) : No typesetting found for |- ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) with typecode |-
46	11	oveqi	$$⊢XHZ=X\mathrm{Hom}\left(C\right)Z$$
47	13 46	eleqtrdi	$$⊢\phi \to M\in \left(X\mathrm{Hom}\left(C\right)Z\right)$$
48	12	oveqi	$$⊢YJW=Y\mathrm{Hom}\left(D\right)W$$
49	14 48	eleqtrdi	$$⊢\phi \to N\in \left(Y\mathrm{Hom}\left(D\right)W\right)$$
50	34 35 36 40 41 47 49	swapf2	Could not format ( ph -> ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = <. N , M >. ) : No typesetting found for |- ( ph -> ( M ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) N ) = <. N , M >. ) with typecode |-
51	45 50	eqtr3id	Could not format ( ph -> ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) = <. N , M >. ) : No typesetting found for |- ( ph -> ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) = <. N , M >. ) with typecode |-
52	44 51	fveq12d	Could not format ( ph -> ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) = ( ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ` <. N , M >. ) ) : No typesetting found for |- ( ph -> ( ( ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ( 2nd ` F ) ( ( 1st ` ( C swapF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C swapF D ) ) <. Z , W >. ) ` <. M , N >. ) ) = ( ( <. Y , X >. ( 2nd ` F ) <. W , Z >. ) ` <. N , M >. ) ) with typecode |-
53	17 30 52	3eqtrd	$$⊢\phi \to M\left(⟨X,Y⟩2^{nd}\left(G\right)⟨Z,W⟩\right)N=\left(⟨Y,X⟩2^{nd}\left(F\right)⟨W,Z⟩\right)\left(⟨N,M⟩\right)$$
54		df-ov	$$⊢N\left(⟨Y,X⟩2^{nd}\left(F\right)⟨W,Z⟩\right)M=\left(⟨Y,X⟩2^{nd}\left(F\right)⟨W,Z⟩\right)\left(⟨N,M⟩\right)$$
55	53 54	eqtr4di	$$⊢\phi \to M\left(⟨X,Y⟩2^{nd}\left(G\right)⟨Z,W⟩\right)N=N\left(⟨Y,X⟩2^{nd}\left(F\right)⟨W,Z⟩\right)M$$