Theorem omf1o

Description: Construct an explicit bijection from A .o B to B .o A . (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypotheses	omf1o.1	$$⊢F=\left(x\in B,y\in A⟼\left(A{\cdot }_{𝑜}x\right){+}_{𝑜}y\right)$$
	omf1o.2	$$⊢G=\left(x\in B,y\in A⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)$$
Assertion	omf1o	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(G\circ F^{-1}\right):A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$

Proof

Step	Hyp	Ref	Expression
1		omf1o.1	$$⊢F=\left(x\in B,y\in A⟼\left(A{\cdot }_{𝑜}x\right){+}_{𝑜}y\right)$$
2		omf1o.2	$$⊢G=\left(x\in B,y\in A⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)$$
3		eqid	$$⊢\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)=\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)$$
4	3	omxpenlem	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right):A\times B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
5	4	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right):A\times B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
6		eqid	$$⊢\left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)=\left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)$$
7	6	xpcomf1o	$$⊢\left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right):B\times A\underset{1-1\; onto}{⟶}A\times B$$
8		f1oco	$$⊢\left(\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right):A\times B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A\wedge \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right):B\times A\underset{1-1\; onto}{⟶}A\times B\right)\to \left(\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)\right):B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
9	5 7 8	sylancl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)\right):B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
10	6 3	xpcomco	$$⊢\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)=\left(x\in B,y\in A⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)$$
11	2 10	eqtr4i	$$⊢G=\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)$$
12		f1oeq1	$$⊢G=\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)\to \left(G:B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A\leftrightarrow \left(\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)\right):B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A\right)$$
13	11 12	ax-mp	$$⊢G:B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A\leftrightarrow \left(\left(y\in A,x\in B⟼\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}x\right)\circ \left(z\in \left(B\times A\right)⟼\bigcup {\left\{z\right\}}^{-1}\right)\right):B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
14	9 13	sylibr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to G:B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
15	1	omxpenlem	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F:B\times A\underset{1-1\; onto}{⟶}A{\cdot }_{𝑜}B$$
16		f1ocnv	$$⊢F:B\times A\underset{1-1\; onto}{⟶}A{\cdot }_{𝑜}B\to F^{-1}:A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B\times A$$
17	15 16	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F^{-1}:A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B\times A$$
18		f1oco	$$⊢\left(G:B\times A\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A\wedge F^{-1}:A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B\times A\right)\to \left(G\circ F^{-1}\right):A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$
19	14 17 18	syl2anc	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(G\circ F^{-1}\right):A{\cdot }_{𝑜}B\underset{1-1\; onto}{⟶}B{\cdot }_{𝑜}A$$