Theorem swapf1f1o

Description: The object part of the swap functor is a bijection between base sets. (Contributed by Zhi Wang, 8-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$$
	swapf1f1o.c	$$⊢\phi \to C\in U$$
	swapf1f1o.d	$$⊢\phi \to D\in V$$
	swapf1f1o.b	$$⊢B={\mathrm{Base}}_S$$
	swapf1f1o.a	$$⊢A={\mathrm{Base}}_T$$
Assertion	swapf1f1o	$$⊢\phi \to O:B\underset{1-1\; onto}{⟶}A$$

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		swapf1f1o.c	$$⊢\phi \to C\in U$$
5		swapf1f1o.d	$$⊢\phi \to D\in V$$
6		swapf1f1o.b	$$⊢B={\mathrm{Base}}_S$$
7		swapf1f1o.a	$$⊢A={\mathrm{Base}}_T$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	2 8 9	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_S$$
11	6 10	eqtr4i	$$⊢B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
12	11	mpteq1i	$$⊢\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
13	12	xpcomf1o	$$⊢\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{Base}}_C\times {\mathrm{Base}}_D\underset{1-1\; onto}{⟶}{\mathrm{Base}}_D\times {\mathrm{Base}}_C$$
14	4 5 2 6 1	swapf1val	$$⊢\phi \to O=\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
15	11	a1i	$$⊢\phi \to B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
16	3 9 8	xpcbas	$$⊢{\mathrm{Base}}_D\times {\mathrm{Base}}_C={\mathrm{Base}}_T$$
17	7 16	eqtr4i	$$⊢A={\mathrm{Base}}_D\times {\mathrm{Base}}_C$$
18	17	a1i	$$⊢\phi \to A={\mathrm{Base}}_D\times {\mathrm{Base}}_C$$
19	14 15 18	f1oeq123d	$$⊢\phi \to \left(O:B\underset{1-1\; onto}{⟶}A\leftrightarrow \left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{Base}}_C\times {\mathrm{Base}}_D\underset{1-1\; onto}{⟶}{\mathrm{Base}}_D\times {\mathrm{Base}}_C\right)$$
20	13 19	mpbiri	$$⊢\phi \to O:B\underset{1-1\; onto}{⟶}A$$