Theorem f1omptsn

Description: A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020)

	Ref	Expression
Hypotheses	f1omptsn.f	$$⊢F=\left(x\in A⟼\left\{x\right\}\right)$$
	f1omptsn.r	$$⊢R=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
Assertion	f1omptsn	$$⊢F:A\underset{1-1\; onto}{⟶}R$$

Proof

Step	Hyp	Ref	Expression
1		f1omptsn.f	$$⊢F=\left(x\in A⟼\left\{x\right\}\right)$$
2		f1omptsn.r	$$⊢R=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
3		sneq	$$⊢x=a\to \left\{x\right\}=\left\{a\right\}$$
4	3	cbvmptv	$$⊢\left(x\in A⟼\left\{x\right\}\right)=\left(a\in A⟼\left\{a\right\}\right)$$
5	4	eqcomi	$$⊢\left(a\in A⟼\left\{a\right\}\right)=\left(x\in A⟼\left\{x\right\}\right)$$
6		id	$$⊢u=z\to u=z$$
7	6 3	eqeqan12d	$$⊢\left(u=z\wedge x=a\right)\to \left(u=\left\{x\right\}\leftrightarrow z=\left\{a\right\}\right)$$
8	7	cbvrexdva	$$⊢u=z\to \left(\exists x\in Au=\left\{x\right\}\leftrightarrow \exists a\in Az=\left\{a\right\}\right)$$
9	8	cbvabv	$$⊢\left\{u|\exists x\in Au=\left\{x\right\}\right\}=\left\{z|\exists a\in Az=\left\{a\right\}\right\}$$
10	9	eqcomi	$$⊢\left\{z|\exists a\in Az=\left\{a\right\}\right\}=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
11	5 10	f1omptsnlem	$$⊢\left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}\left\{z|\exists a\in Az=\left\{a\right\}\right\}$$
12	2 9	eqtri	$$⊢R=\left\{z|\exists a\in Az=\left\{a\right\}\right\}$$
13		f1oeq3	$$⊢R=\left\{z|\exists a\in Az=\left\{a\right\}\right\}\to \left(\left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}R\leftrightarrow \left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}\left\{z|\exists a\in Az=\left\{a\right\}\right\}\right)$$
14	12 13	ax-mp	$$⊢\left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}R\leftrightarrow \left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}\left\{z|\exists a\in Az=\left\{a\right\}\right\}$$
15	11 14	mpbir	$$⊢\left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}R$$
16	1 4	eqtri	$$⊢F=\left(a\in A⟼\left\{a\right\}\right)$$
17		f1oeq1	$$⊢F=\left(a\in A⟼\left\{a\right\}\right)\to \left(F:A\underset{1-1\; onto}{⟶}R\leftrightarrow \left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}R\right)$$
18	16 17	ax-mp	$$⊢F:A\underset{1-1\; onto}{⟶}R\leftrightarrow \left(a\in A⟼\left\{a\right\}\right):A\underset{1-1\; onto}{⟶}R$$
19	15 18	mpbir	$$⊢F:A\underset{1-1\; onto}{⟶}R$$