Theorem swapf2f1oa

Description: The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 9-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)$$
	swapf2f1oa.b	$$⊢B={\mathrm{Base}}_S$$
	swapf2f1oa.x	$$⊢\phi \to X\in B$$
	swapf2f1oa.y	$$⊢\phi \to Y\in B$$
Assertion	swapf2f1oa	$$⊢\phi \to \left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)$$

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		swapf2f1oa.b	$$⊢B={\mathrm{Base}}_S$$
7		swapf2f1oa.x	$$⊢\phi \to X\in B$$
8		swapf2f1oa.y	$$⊢\phi \to Y\in B$$
9		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
10		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
11	2 9 10	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_S$$
12	6 11	eqtr4i	$$⊢B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
13	7 12	eleqtrdi	$$⊢\phi \to X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
14		xp1st	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
15	13 14	syl	$$⊢\phi \to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
16		xp2nd	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
17	13 16	syl	$$⊢\phi \to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
18	8 12	eleqtrdi	$$⊢\phi \to Y\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
19		xp1st	$$⊢Y\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 1^{st}\left(Y\right)\in {\mathrm{Base}}_C$$
20	18 19	syl	$$⊢\phi \to 1^{st}\left(Y\right)\in {\mathrm{Base}}_C$$
21		xp2nd	$$⊢Y\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 2^{nd}\left(Y\right)\in {\mathrm{Base}}_D$$
22	18 21	syl	$$⊢\phi \to 2^{nd}\left(Y\right)\in {\mathrm{Base}}_D$$
23	1 2 3 4 5 15 17 20 22	swapf2f1o	$$⊢\phi \to \left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩\right):⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩H⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩\underset{1-1\; onto}{⟶}⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩J⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩$$
24		1st2nd2	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩$$
25	13 24	syl	$$⊢\phi \to X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩$$
26		1st2nd2	$$⊢Y\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to Y=⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩$$
27	18 26	syl	$$⊢\phi \to Y=⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩$$
28	25 27	oveq12d	$$⊢\phi \to XPY=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩$$
29	25 27	oveq12d	$$⊢\phi \to XHY=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩H⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩$$
30	1 2 6 7	swapf1a	$$⊢\phi \to O\left(X\right)=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
31	1 2 6 8	swapf1a	$$⊢\phi \to O\left(Y\right)=⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩$$
32	30 31	oveq12d	$$⊢\phi \to O\left(X\right)JO\left(Y\right)=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩J⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩$$
33	28 29 32	f1oeq123d	$$⊢\phi \to \left(\left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)\leftrightarrow \left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩\right):⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩H⟨1^{st}\left(Y\right),2^{nd}\left(Y\right)⟩\underset{1-1\; onto}{⟶}⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩J⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩\right)$$
34	23 33	mpbird	$$⊢\phi \to \left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)$$