Metamath Proof Explorer

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 = (x \in A ⟼ \{x\})$
		f1omptsn.r	$⊢ R = \{u \| \exists x \in A u = \{x\}\}$
	Assertion	f1omptsn	$⊢ F : A \underset{1-1 onto}{⟶} R$

Proof

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