Derangements

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}_{0}$, let $[n]$ be as in Intervals of Natural Numbers (ii), and let $S_{n}$ be the set of permutations of $[n]$ (Permutations of a Set and the Set of Permutations of [n] (iii)).

(i) Derangement. A derangement of $[n]$ is a permutation $\sigma\in S_{n}$ with

$$\sigma(i)\neq i\quad\text{for every }i\in[n].$$

(ii) The set of derangements. The set of derangements of $[n]$ is

$$D_{n}=\{\sigma\in S_{n}:\sigma(i)\neq i\text{ for every }i\in[n]\},$$

a subset of $S_{n}$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)).