Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let finite and infinite sets be as in Finite Sets §finite, $\#$ as in The Number of Elements of a Finite Set §cardinality, and $[n]$ as in Intervals of Natural Numbers §segment; subsets of finite sets and the sets $[n]$ are finite by 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 §subset and 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 §naturals.

¶ If $B$ is a finite set and $x\in B$, then $\#B=\#(B\setminus\{x\})+1$.

¶ If $A$ is a finite set, every injective map $f:A\to A$ is a bijection.

¶ $\mathbb{N}$ is infinite, and so is every set $X$ for which there is an injective map from $\mathbb{N}$ to $X$.

¶ For $n\in\mathbb{N}_{0}$, the set $S_{n}$ of permutations of $[n]$ is finite and nonempty.

¶ For sets $a$ and $B$, the map $b\mapsto(a,b)$ is a bijection from $B$ onto $\{a\}\times B$.

¶ Let $Y$ be a set, $n\in\mathbb{N}_{0}$, and let $Y^{n}$ and the components of its elements be as in Tuples in a Set: the Set of n-Tuples and Their Components §tuples and Tuples in a Set: the Set of n-Tuples and Their Components §components. For $t\in Y^{n}$ and $y\in Y$ there is exactly one $u\in Y^{n+1}$ with $u_{k}=t_{k}$ for $k\in[n]$ and $u_{n+1}=y$, and the map $(t,y)\mapsto u$ is a bijection from $Y^{n}\times Y$ onto $Y^{n+1}$.