Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice

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, intervals and $[n]$ as in Intervals of Natural Numbers §interval and Intervals of Natural Numbers §segment, and let $A$ and $B$ be sets.

¶ 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$.

¶ If $A$ is finite, every subset of $A$ is finite.

¶ If $A$ and $B$ are finite, then $A\cup B$ and $A\times B$ are finite.

¶ If $A$ is finite and $f:A\to B$ is a map, then $f(A)$ is finite.

¶ A subset $S$ of $\mathbb{N}_{0}$ is finite if and only if there is $b\in\mathbb{N}_{0}$ with $k\le b$ for every $k\in S$; in particular every interval $\{m,\dots,n\}$ with $m,n\in\mathbb{N}_{0}$ is finite.

¶ Let $\le$ be a total order on a set $X$. Every nonempty finite subset $S$ of $X$ has a greatest element and a least element, $\max S$ and $\min S$ of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least.

¶ If $A$ and $B$ are finite, then the set $B^{A}$ of maps from $A$ to $B$ is finite; if moreover $B\neq\emptyset$, then $B^{A}\neq\emptyset$.

Let now $I$ be a finite set and $(C_{i})_{i\in I}$ a family of sets, with union $\bigcup_{i\in I}C_{i}$ as in Indexed Families of Sets and Their Union, Intersection and Product §union, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union.

¶ If $C_{i}$ is finite for every $i\in I$, then $\bigcup_{i\in I}C_{i}$ is finite.

¶ If $C_{i}\neq\emptyset$ for every $i\in I$, then there is a map $f:I\to\bigcup_{i\in I}C_{i}$ with $f(i)\in C_{i}$ for every $i\in I$.