ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2764 on D468: Bijective map
Canonical singleton map is bijection
Formulation 0
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}
Then $f$ is a D468: Bijective map from $X$ to $\{ \{ x \} : x \in X \}$.
Formulation 1
Let $X$ be a D11: Set such that
(i) $f : X \to \{ \{ x \} : x \in X \}$ is the D4493: Canonical singleton map on $X$
Then $f$ is a D468: Bijective map from $X$ to $\{ \{ x \} : x \in X \}$.
Proofs
Proof 0
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$