Theorem swapf1

Description: The object part of the swap functor swaps the objects. (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$$
Assertion	swapf1	$$⊢\phi \to XOY=⟨Y,X⟩$$

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		df-ov	$$⊢XOY=O\left(⟨X,Y⟩\right)$$
5	2	elfvexd	$$⊢\phi \to C\in \mathrm{V}$$
6	3	elfvexd	$$⊢\phi \to D\in \mathrm{V}$$
7		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	7 8 9	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
11	5 6 7 10 1	swapf1val	$$⊢\phi \to O=\left(x\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
12		simpr	$$⊢\left(\phi \wedge x=⟨X,Y⟩\right)\to x=⟨X,Y⟩$$
13	12	sneqd	$$⊢\left(\phi \wedge x=⟨X,Y⟩\right)\to \left\{x\right\}=\left\{⟨X,Y⟩\right\}$$
14	13	cnveqd	$$⊢\left(\phi \wedge x=⟨X,Y⟩\right)\to {\left\{x\right\}}^{-1}={\left\{⟨X,Y⟩\right\}}^{-1}$$
15	14	unieqd	$$⊢\left(\phi \wedge x=⟨X,Y⟩\right)\to \bigcup {\left\{x\right\}}^{-1}=\bigcup {\left\{⟨X,Y⟩\right\}}^{-1}$$
16		opswap	$$⊢\bigcup {\left\{⟨X,Y⟩\right\}}^{-1}=⟨Y,X⟩$$
17	15 16	eqtrdi	$$⊢\left(\phi \wedge x=⟨X,Y⟩\right)\to \bigcup {\left\{x\right\}}^{-1}=⟨Y,X⟩$$
18	2 3	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
19		opex	$$⊢⟨Y,X⟩\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to ⟨Y,X⟩\in \mathrm{V}$$
21	11 17 18 20	fvmptd	$$⊢\phi \to O\left(⟨X,Y⟩\right)=⟨Y,X⟩$$
22	4 21	eqtrid	$$⊢\phi \to XOY=⟨Y,X⟩$$