The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let finite sets be as in Finite Sets §finite and $[n]$ as in Intervals of Natural Numbers §segment, and let $A$ be a set.

¶ Let $m,n\in\mathbb{N}_{0}$. If there is an injective map from $[m]$ to $[n]$, then $m\le n$; if there is a bijection from $[m]$ onto $[n]$, then $m=n$.

¶ If $A$ is finite, there is exactly one $n\in\mathbb{N}_{0}$ for which there is a bijection from $[n]$ onto $A$.

¶ $\emptyset$ is finite, and $\{x\}$ is finite for every set $x$.