Theorem swapf2a

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

	Ref	Expression
Hypotheses	swapf1a.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
	swapf1a.s	$$⊢S=C{\times }_{c}D$$
	swapf1a.b	$$⊢B={\mathrm{Base}}_S$$
	swapf1a.x	$$⊢\phi \to X\in B$$
	swapf2a.y	$$⊢\phi \to Y\in B$$
	swapf2a.h	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
	swapf2a.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	swapf2a	$$⊢\phi \to \left(XPY\right)\left(F\right)=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		swapf1a.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
2		swapf1a.s	$$⊢S=C{\times }_{c}D$$
3		swapf1a.b	$$⊢B={\mathrm{Base}}_S$$
4		swapf1a.x	$$⊢\phi \to X\in B$$
5		swapf2a.y	$$⊢\phi \to Y\in B$$
6		swapf2a.h	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
7		swapf2a.f	$$⊢\phi \to F\in \left(XHY\right)$$
8	1 2 3 4 5 6	swapf2vala	$$⊢\phi \to XPY=\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
9		simpr	$$⊢\left(\phi \wedge f=F\right)\to f=F$$
10	9	sneqd	$$⊢\left(\phi \wedge f=F\right)\to \left\{f\right\}=\left\{F\right\}$$
11	10	cnveqd	$$⊢\left(\phi \wedge f=F\right)\to {\left\{f\right\}}^{-1}={\left\{F\right\}}^{-1}$$
12	11	unieqd	$$⊢\left(\phi \wedge f=F\right)\to \bigcup {\left\{f\right\}}^{-1}=\bigcup {\left\{F\right\}}^{-1}$$
13	6	oveqd	$$⊢\phi \to XHY=X\mathrm{Hom}\left(S\right)Y$$
14		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
15		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
16		eqid	$$⊢\mathrm{Hom}\left(S\right)=\mathrm{Hom}\left(S\right)$$
17	2 3 14 15 16 4 5	xpchom	$$⊢\phi \to X\mathrm{Hom}\left(S\right)Y=\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)$$
18	13 17	eqtrd	$$⊢\phi \to XHY=\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)$$
19	7 18	eleqtrd	$$⊢\phi \to F\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)$$
20		2nd1st	$$⊢F\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)\to \bigcup {\left\{F\right\}}^{-1}=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$
21	19 20	syl	$$⊢\phi \to \bigcup {\left\{F\right\}}^{-1}=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$
22	21	adantr	$$⊢\left(\phi \wedge f=F\right)\to \bigcup {\left\{F\right\}}^{-1}=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$
23	12 22	eqtrd	$$⊢\left(\phi \wedge f=F\right)\to \bigcup {\left\{f\right\}}^{-1}=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$
24		opex	$$⊢⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to ⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩\in \mathrm{V}$$
26	8 23 7 25	fvmptd	$$⊢\phi \to \left(XPY\right)\left(F\right)=⟨2^{nd}\left(F\right),1^{st}\left(F\right)⟩$$