Countable iff Cardinality not greater than Aleph Zero

Theorem

Let $X$ be set.

$X$ is countable if and only if: $\card X \le \aleph_0$

where:

$\card X$ denotes the cardinality of $X$

$\aleph_0 = \card \N$ by Aleph Zero equals Cardinality of Naturals.

Proof

$X$ is countable

if and only if:

there exists an injection $f: X \to \N$ by definition of countable set

if and only if:

$\card X \le \card \N$ by Injection iff Cardinal Inequality

if and only if:

$\card X \le \aleph_0$

$\blacksquare$

Sources

• Mizar article CARD_3:def 14