Theorem swapf2val

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$$
	swapf2val.s	$$⊢S=C{\times }_{c}D$$
	swapf2val.h	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
Assertion	swapf2val	$$⊢\phi \to ⟨X,Y⟩P⟨Z,W⟩=\left(f\in \left(⟨X,Y⟩H⟨Z,W⟩\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$

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		swapf2val.s	$$⊢S=C{\times }_{c}D$$
7		swapf2val.h	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	6 8 9	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_S$$
11	2 3	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
12	4 5	opelxpd	$$⊢\phi \to ⟨Z,W⟩\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
13	1 6 10 11 12 7	swapf2vala	$$⊢\phi \to ⟨X,Y⟩P⟨Z,W⟩=\left(f\in \left(⟨X,Y⟩H⟨Z,W⟩\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$