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}

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

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$

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$