Theorem oacomf1o

Description: Define a bijection from A +o B to B +o A . Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g., oancom ). (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypothesis	oacomf1o.1	$$⊢F=\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}$$
Assertion	oacomf1o	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}B{+}_{𝑜}A$$

Proof

Step	Hyp	Ref	Expression
1		oacomf1o.1	$$⊢F=\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}$$
2		eqid	$$⊢\left(x\in A⟼B{+}_{𝑜}x\right)=\left(x\in A⟼B{+}_{𝑜}x\right)$$
3	2	oacomf1olem	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(x\in A⟼B{+}_{𝑜}x\right):A\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\wedge \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cap B=\varnothing \right)$$
4	3	simpld	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(x\in A⟼B{+}_{𝑜}x\right):A\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)$$
5		eqid	$$⊢\left(x\in B⟼A{+}_{𝑜}x\right)=\left(x\in B⟼A{+}_{𝑜}x\right)$$
6	5	oacomf1olem	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(\left(x\in B⟼A{+}_{𝑜}x\right):B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\wedge \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\cap A=\varnothing \right)$$
7	6	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(x\in B⟼A{+}_{𝑜}x\right):B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\wedge \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\cap A=\varnothing \right)$$
8	7	simpld	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(x\in B⟼A{+}_{𝑜}x\right):B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$
9		f1ocnv	$$⊢\left(x\in B⟼A{+}_{𝑜}x\right):B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\to {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}:\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}B$$
10	8 9	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}:\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}B$$
11		incom	$$⊢A\cap \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\cap A$$
12	7	simprd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\cap A=\varnothing$$
13	11 12	syl5eq	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\cap \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)=\varnothing$$
14	3	simprd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cap B=\varnothing$$
15		f1oun	$$⊢\left(\left(\left(x\in A⟼B{+}_{𝑜}x\right):A\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\wedge {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}:\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}B\right)\wedge \left(A\cap \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)=\varnothing \wedge \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cap B=\varnothing \right)\right)\to \left(\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}\right):A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
16	4 10 13 14 15	syl22anc	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}\right):A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
17		f1oeq1	$$⊢F=\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}\to \left(F:A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\leftrightarrow \left(\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}\right):A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\right)$$
18	1 17	ax-mp	$$⊢F:A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\leftrightarrow \left(\left(x\in A⟼B{+}_{𝑜}x\right)\cup {\left(x\in B⟼A{+}_{𝑜}x\right)}^{-1}\right):A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
19	16 18	sylibr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F:A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
20		oarec	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A{+}_{𝑜}B=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$
21	20	f1oeq2d	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\leftrightarrow F:A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\right)$$
22	19 21	mpbird	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
23		oarec	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to B{+}_{𝑜}A=B\cup \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)$$
24	23	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to B{+}_{𝑜}A=B\cup \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)$$
25		uncom	$$⊢B\cup \mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
26	24 25	eqtrdi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to B{+}_{𝑜}A=\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B$$
27	26	f1oeq3d	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}B{+}_{𝑜}A\leftrightarrow F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in A⟼B{+}_{𝑜}x\right)\cup B\right)$$
28	22 27	mpbird	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to F:A{+}_{𝑜}B\underset{1-1\; onto}{⟶}B{+}_{𝑜}A$$