Theorem swapf1a

Description: The object part of the swap functor swaps the objects. (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$$
Assertion	swapf1a	$$⊢\phi \to O\left(X\right)=⟨2^{nd}\left(X\right),1^{st}\left(X\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	2 3 4	elxpcbasex1	$$⊢\phi \to C\in \mathrm{V}$$
6	2 3 4	elxpcbasex2	$$⊢\phi \to D\in \mathrm{V}$$
7	5 6 2 3 1	swapf1val	$$⊢\phi \to O=\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
8		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
9	8	sneqd	$$⊢\left(\phi \wedge x=X\right)\to \left\{x\right\}=\left\{X\right\}$$
10	9	cnveqd	$$⊢\left(\phi \wedge x=X\right)\to {\left\{x\right\}}^{-1}={\left\{X\right\}}^{-1}$$
11	10	unieqd	$$⊢\left(\phi \wedge x=X\right)\to \bigcup {\left\{x\right\}}^{-1}=\bigcup {\left\{X\right\}}^{-1}$$
12		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
13		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
14	2 12 13	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_S$$
15	3 14	eqtr4i	$$⊢B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
16	4 15	eleqtrdi	$$⊢\phi \to X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
17		2nd1st	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to \bigcup {\left\{X\right\}}^{-1}=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
18	16 17	syl	$$⊢\phi \to \bigcup {\left\{X\right\}}^{-1}=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
19	18	adantr	$$⊢\left(\phi \wedge x=X\right)\to \bigcup {\left\{X\right\}}^{-1}=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
20	11 19	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to \bigcup {\left\{x\right\}}^{-1}=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
21		opex	$$⊢⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to ⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\in \mathrm{V}$$
23	7 20 4 22	fvmptd	$$⊢\phi \to O\left(X\right)=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$