Theorem cnvf1o

Description: Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Assertion	cnvf1o	$$⊢\mathrm{Rel}A\to \left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right):A\underset{1-1\; onto}{⟶}{A}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
2		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
3	2	cnvex	$$⊢{\left\{x\right\}}^{-1}\in \mathrm{V}$$
4	3	uniex	$$⊢\bigcup {\left\{x\right\}}^{-1}\in \mathrm{V}$$
5	4	a1i	$$⊢\left(\mathrm{Rel}A\wedge x\in A\right)\to \bigcup {\left\{x\right\}}^{-1}\in \mathrm{V}$$
6		snex	$$⊢\left\{y\right\}\in \mathrm{V}$$
7	6	cnvex	$$⊢{\left\{y\right\}}^{-1}\in \mathrm{V}$$
8	7	uniex	$$⊢\bigcup {\left\{y\right\}}^{-1}\in \mathrm{V}$$
9	8	a1i	$$⊢\left(\mathrm{Rel}A\wedge y\in A^{-1}\right)\to \bigcup {\left\{y\right\}}^{-1}\in \mathrm{V}$$
10		cnvf1olem	$$⊢\left(\mathrm{Rel}A\wedge \left(x\in A\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\right)\to \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)$$
11		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
12		simpr	$$⊢\left(\mathrm{Rel}A\wedge \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)\to \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)$$
13		cnvf1olem	$$⊢\left(\mathrm{Rel}{A}^{-1}\wedge \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)\to \left(x\in {A^{-1}}^{-1}\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)$$
14	11 12 13	sylancr	$$⊢\left(\mathrm{Rel}A\wedge \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)\to \left(x\in {A^{-1}}^{-1}\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)$$
15		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
16		eleq2	$$⊢{A^{-1}}^{-1}=A\to \left(x\in {A^{-1}}^{-1}\leftrightarrow x\in A\right)$$
17	15 16	sylbi	$$⊢\mathrm{Rel}A\to \left(x\in {A^{-1}}^{-1}\leftrightarrow x\in A\right)$$
18	17	anbi1d	$$⊢\mathrm{Rel}A\to \left(\left(x\in {A^{-1}}^{-1}\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\leftrightarrow \left(x\in A\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
19	18	adantr	$$⊢\left(\mathrm{Rel}A\wedge \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)\to \left(\left(x\in {A^{-1}}^{-1}\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\leftrightarrow \left(x\in A\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
20	14 19	mpbid	$$⊢\left(\mathrm{Rel}A\wedge \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)\to \left(x\in A\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)$$
21	10 20	impbida	$$⊢\mathrm{Rel}A\to \left(\left(x\in A\wedge y=\bigcup {\left\{x\right\}}^{-1}\right)\leftrightarrow \left(y\in A^{-1}\wedge x=\bigcup {\left\{y\right\}}^{-1}\right)\right)$$
22	1 5 9 21	f1od	$$⊢\mathrm{Rel}A\to \left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right):A\underset{1-1\; onto}{⟶}{A}^{-1}$$