Basic Properties of Finite Sets

Let $\mathbb{N}$ be the set of natural numbers with successor map $S$, let $\le$ be the order on $\mathbb{N}$, let $[n]$ denote the initial segment determined by $n$, and let the notions number of elements $|X|$ and finite be as in those definitions. Then the following hold.

1. For every $n\in\mathbb{N}$ the set $[n]$ has $n$ elements.
2. For every object $x$ the set $\{x\}$ has $1$ element. If $A$ has $k$ elements and $x\notin A$, then $A\cup\{x\}$ has $S(k)$ elements.
3. If $X$ is finite and $A\subseteq X$, then $A$ is finite. If moreover $X$ has $n$ elements and $A\ne\emptyset$, then $A$ has $m$ elements for some $m\le n$.
4. If $X$ has $n$ elements, $Y$ is a set, and $q:X\to Y$ is surjective (that is, every $y\in Y$ equals $q(x)$ for some $x\in X$), then $Y$ has $m$ elements for some $m\le n$; in particular $Y$ is finite and nonempty.