ThmDex – An index of mathematical definitions, results, and conjectures.
Result R371 on D16: Countable set
Countable set iff injection to natural numbers
Formulation 0
Let $X$ be a D11: Set.
Then $X$ is a D16: Countable set if and only if \begin{equation} \mathsf{Inj}(X \to \mathbb{N}) \neq \emptyset \end{equation}
Proofs
Proof 0
Let $X$ be a D11: Set.
If $X$ is countable, then there exists a bijection $f : X \to E$ for some $E \subseteq \mathbb{N}$ and a bijection is also an injection.

Suppose then that there exists an injection $f : X \to \mathbb{N}$. Then the D1079: Canonical surjective submap $F : X \to f(X)$ is a bijection. Since $f(X) \subseteq \mathbb{N}$, result R433: Subset of countable set is countable says that $f(X)$ is countable. Since $F$ is a bijection, $|X| = |f(X)|$ and therefore $X$ is countable. $\square$