Theorem swapf2f1o

Description: The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 8-Oct-2025)

	Ref	Expression
Hypotheses	swapf1f1o.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
	swapf1f1o.s	$$⊢S=C{\times }_{c}D$$
	swapf1f1o.t	$$⊢T=D{\times }_{c}C$$
	swapf2f1o.h	$$⊢H=\mathrm{Hom}\left(S\right)$$
	swapf2f1o.j	$$⊢J=\mathrm{Hom}\left(T\right)$$
	swapf2f1o.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
	swapf2f1o.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
	swapf2f1o.z	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
	swapf2f1o.w	$$⊢\phi \to W\in {\mathrm{Base}}_D$$
Assertion	swapf2f1o	$$⊢\phi \to \left(⟨X,Y⟩P⟨Z,W⟩\right):⟨X,Y⟩H⟨Z,W⟩\underset{1-1\; onto}{⟶}⟨Y,X⟩J⟨W,Z⟩$$

Proof

Step	Hyp	Ref	Expression
1		swapf1f1o.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
2		swapf1f1o.s	$$⊢S=C{\times }_{c}D$$
3		swapf1f1o.t	$$⊢T=D{\times }_{c}C$$
4		swapf2f1o.h	$$⊢H=\mathrm{Hom}\left(S\right)$$
5		swapf2f1o.j	$$⊢J=\mathrm{Hom}\left(T\right)$$
6		swapf2f1o.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
7		swapf2f1o.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
8		swapf2f1o.z	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
9		swapf2f1o.w	$$⊢\phi \to W\in {\mathrm{Base}}_D$$
10		eqid	$$⊢\left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
11	10	xpcomf1o	$$⊢\left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right):\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\underset{1-1\; onto}{⟶}\left(Y\mathrm{Hom}\left(D\right)W\right)\times \left(X\mathrm{Hom}\left(C\right)Z\right)$$
12	4	a1i	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
13	1 6 7 8 9 2 12	swapf2val	$$⊢\phi \to ⟨X,Y⟩P⟨Z,W⟩=\left(f\in \left(⟨X,Y⟩H⟨Z,W⟩\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
14		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
15		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
16		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
17		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
18	2 14 15 16 17 6 7 8 9 4	xpchom2	$$⊢\phi \to ⟨X,Y⟩H⟨Z,W⟩=\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)$$
19	18	mpteq1d	$$⊢\phi \to \left(f\in \left(⟨X,Y⟩H⟨Z,W⟩\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
20	13 19	eqtrd	$$⊢\phi \to ⟨X,Y⟩P⟨Z,W⟩=\left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
21	3 15 14 17 16 7 6 9 8 5	xpchom2	$$⊢\phi \to ⟨Y,X⟩J⟨W,Z⟩=\left(Y\mathrm{Hom}\left(D\right)W\right)\times \left(X\mathrm{Hom}\left(C\right)Z\right)$$
22	20 18 21	f1oeq123d	$$⊢\phi \to \left(\left(⟨X,Y⟩P⟨Z,W⟩\right):⟨X,Y⟩H⟨Z,W⟩\underset{1-1\; onto}{⟶}⟨Y,X⟩J⟨W,Z⟩\leftrightarrow \left(f\in \left(\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right):\left(X\mathrm{Hom}\left(C\right)Z\right)\times \left(Y\mathrm{Hom}\left(D\right)W\right)\underset{1-1\; onto}{⟶}\left(Y\mathrm{Hom}\left(D\right)W\right)\times \left(X\mathrm{Hom}\left(C\right)Z\right)\right)$$
23	11 22	mpbiri	$$⊢\phi \to \left(⟨X,Y⟩P⟨Z,W⟩\right):⟨X,Y⟩H⟨Z,W⟩\underset{1-1\; onto}{⟶}⟨Y,X⟩J⟨W,Z⟩$$