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$
