Theorem swapf2vala

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)$$
Assertion	swapf2vala	$$⊢\phi \to XPY=\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\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	2 3 4	elxpcbasex1	$$⊢\phi \to C\in \mathrm{V}$$
8	2 3 4	elxpcbasex2	$$⊢\phi \to D\in \mathrm{V}$$
9	7 8 2 3 6 1	swapf2fval	$$⊢\phi \to P=\left(u\in B,v\in B⟼\left(f\in \left(uHv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
10		simprl	$$⊢\left(\phi \wedge \left(u=X\wedge v=Y\right)\right)\to u=X$$
11		simprr	$$⊢\left(\phi \wedge \left(u=X\wedge v=Y\right)\right)\to v=Y$$
12	10 11	oveq12d	$$⊢\left(\phi \wedge \left(u=X\wedge v=Y\right)\right)\to uHv=XHY$$
13	12	mpteq1d	$$⊢\left(\phi \wedge \left(u=X\wedge v=Y\right)\right)\to \left(f\in \left(uHv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
14		ovex	$$⊢XHY\in \mathrm{V}$$
15	14	mptex	$$⊢\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\in \mathrm{V}$$
17	9 13 4 5 16	ovmpod	$$⊢\phi \to XPY=\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$