Let $X$ be a
D11: Set.
Let $f : X \to \{ \{ x \} : x \in X \}$ be a
D18: Map such that
(i) |
\begin{equation}
f(x) : = \{ x \}
\end{equation}
|
Set $Y : = \{ \{ x \} : x \in X \}$. If $X$ is empty, then $Y$ is also empty and the claim is a consequence of
R2766: Canonical empty map is bijection.
Suppose thus that $X$ is nonempty and let $x, y \in X$ be such that $f(x) = f(y)$. Then $\{ x \} = f(x) = f(y) = \{ y \}$, whence $x = y$, so that $f$ is injective.
If $y \in Y$, then $y = \{ x \}$ for some $x \in X$ such that $f(x) = \{ x \} = y$, so $f$ is also surjective. Since $f$ is both an injection and a surjection, that $f$ is a bijection then follows from
R1478: Equivalent characterisations of bijectivity. $\square$