Theorem swapf2

Description: The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapf1.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
	swapf1.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
	swapf1.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
	swapf2.z	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
	swapf2.w	$$⊢\phi \to W\in {\mathrm{Base}}_D$$
	swapf2.f	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Z\right)$$
	swapf2.g	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(D\right)W\right)$$
Assertion	swapf2	$$⊢\phi \to F\left(⟨X,Y⟩P⟨Z,W⟩\right)G=⟨G,F⟩$$

Proof

Step	Hyp	Ref	Expression
1		swapf1.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
2		swapf1.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
3		swapf1.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
4		swapf2.z	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
5		swapf2.w	$$⊢\phi \to W\in {\mathrm{Base}}_D$$
6		swapf2.f	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Z\right)$$
7		swapf2.g	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(D\right)W\right)$$
8		df-ov	$$⊢F\left(⟨X,Y⟩P⟨Z,W⟩\right)G=\left(⟨X,Y⟩P⟨Z,W⟩\right)\left(⟨F,G⟩\right)$$
9		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
10		eqidd	$$⊢\phi \to \mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
11	1 2 3 4 5 9 10	swapf2val	$$⊢\phi \to ⟨X,Y⟩P⟨Z,W⟩=\left(f\in \left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Z,W⟩\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
12		simpr	$$⊢\left(\phi \wedge f=⟨F,G⟩\right)\to f=⟨F,G⟩$$
13	12	sneqd	$$⊢\left(\phi \wedge f=⟨F,G⟩\right)\to \left\{f\right\}=\left\{⟨F,G⟩\right\}$$
14	13	cnveqd	$$⊢\left(\phi \wedge f=⟨F,G⟩\right)\to {\left\{f\right\}}^{-1}={\left\{⟨F,G⟩\right\}}^{-1}$$
15	14	unieqd	$$⊢\left(\phi \wedge f=⟨F,G⟩\right)\to \bigcup {\left\{f\right\}}^{-1}=\bigcup {\left\{⟨F,G⟩\right\}}^{-1}$$
16		opswap	$$⊢\bigcup {\left\{⟨F,G⟩\right\}}^{-1}=⟨G,F⟩$$
17	15 16	eqtrdi	$$⊢\left(\phi \wedge f=⟨F,G⟩\right)\to \bigcup {\left\{f\right\}}^{-1}=⟨G,F⟩$$
18	6 7	opelxpd	$$⊢\phi \to ⟨F,G⟩\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)$$
19		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
20		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
21		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
22		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
23		eqid	$$⊢\mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
24	9 19 20 21 22 2 3 4 5 23	xpchom2	$$⊢\phi \to ⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Z,W⟩=\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)$$
25	18 24	eleqtrrd	$$⊢\phi \to ⟨F,G⟩\in \left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Z,W⟩\right)$$
26		opex	$$⊢⟨G,F⟩\in \mathrm{V}$$
27	26	a1i	$$⊢\phi \to ⟨G,F⟩\in \mathrm{V}$$
28	11 17 25 27	fvmptd	$$⊢\phi \to \left(⟨X,Y⟩P⟨Z,W⟩\right)\left(⟨F,G⟩\right)=⟨G,F⟩$$
29	8 28	eqtrid	$$⊢\phi \to F\left(⟨X,Y⟩P⟨Z,W⟩\right)G=⟨G,F⟩$$