Definition of finiteness

We define a set $\mathbb{B}$ to be finite if and only either

• $\mathbb{B}$ is empty, in which case we say that the set $\mathbb{B}$ has zero elements,

or

• there is a bijection of $\mathbb{B}$ with $\mathbb{N}_k$ for some positive integer $k$, in which case we say that $\mathbb{B}$ has $k$ elements.

Using this language, we have proved above:

• (E)
  If $\mathbb{B}$ is a non-empty set and there is an injection $f: \mathbb{B}\rightarrow \mathbb{N}_n$, for some positive integer $n$, then $\mathbb{B}$ is a finite set.
  Also either $f$ is a bijection or $n > 1$ and $\mathbb{B}$ has fewer than $n$ elements.
• (F)
  If $\mathbb{C}$ is a non-empty set and there is a surjection $p: \mathbb{N}_m \rightarrow \mathbb{C}$, for some positive integer $m$, then $\mathbb{C}$ is a finite set.
  Also either $p$ is a bijection or $m > 1$ and $\mathbb{C}$ has fewer than $m$ elements.

The following corollaries follow immediately:

• (G)
  If $f: \mathbb{C} \rightarrow \mathbb{B}$ is an injection of non-empty sets, then if $\mathbb{B}$ is finite, so is $\mathbb{C}$.
  Also either $f$ is a bijection, or the number of elements of $\mathbb{C}$ is less than that of $\mathbb{B}$.
• (H)
  If $p: \mathbb{B} \rightarrow \mathbb{C}$ is an surjection of non-empty sets, then if $\mathbb{B}$ is finite, so is $\mathbb{C}$.
  Also either $p$ is a bijection, or the number of elements of $\mathbb{C}$ is less than that of $\mathbb{B}$.