Injections into $\mathbb{N}_n$

We prove the following results:

• (A)
  Let a non-empty set $\mathbb{A}$ be given.
  Suppose that there exists an $n \in\mathbb{N}$, and an injection $f: \mathbb{A}\rightarrow \mathbb{N}_n$.
  Then either $f$ is a bijection, or $n > 1$ and there exists an injection $g: \mathbb{A}\rightarrow \mathbb{N}_{n - 1}$.

Proof:
If $n = 1$, then $\mathbb{N}_1 = \{1\}$ and any map from a non-empty set to $\mathbb{N}_1$ is automatically surjective, so $f$ is a bijection and we are done.
So we may assume that $n > 1$ and that $f$ is not a bijection, since otherwise we are done.
We need to construct the injective map $g$.
Since $f$ is not surjective there exists $k \in \mathbb{N}_n$, such that $k \notin f(\mathbb{A})$.
Pick such a $k$ and define the map $g: \mathbb{A}\rightarrow \mathbb{N}_n$ by the composition: $g = S_{k, n} \circ f$.
Since $S_{k, n}$ is a bijection and $f$ an injection, $g$ is an injection also.
Since $S_{k, n}$ is its own inverse, we have: $S_{k, n} \circ g = f$.
Suppose that some $x \in \mathbb{A}$ exists such that $g(x) = n$.
Then we have:

$$f(x) = (S_{k, n}\circ g)(x) = S_{k, n}(g(x)) = S_{k, n}(n) = k.$$

So $k \in f(\mathbb{A})$, a contradiction, so $n \notin g(\mathbb{A})$.
So $g(\mathbb{A}) \subset \mathbb{N}_{n - 1}$.
So the map $g$ restricts to a well-defined map from $\mathbb{A}$ to $\mathbb{N}_{n - 1}$ and $g$ being injective as a map from $\mathbb{A}$ to $\mathbb{N}_n$ is automatically injective also as a map from $\mathbb{A}\rightarrow \mathbb{N}_{n-1}$ and we are done.

By the Well Ordering Principle, we have the following corollary:

• (B)
  Let $\mathbb{A}$ be a non-empty set and $f: \mathbb{A}\rightarrow \mathbb{N}_n$ an injection, for some $n \in\mathbb{N}$.
  Then either $f$ is a bijection, or $n > 1$ and there exists $m \in \mathbb{N}$, with $m < n$ and a bijection $g: \mathbb{A} \rightarrow \mathbb{N}_m$.

Proof:
Here $m \ge 1$ is the least integer such that an injection $g: \mathbb{A} \rightarrow \mathbb{N}_m$ exists.
Then $g$ is bijective, since otherwise we could lower the integer $m$, by (A).