Let $X$ be a D17: Finite set such that

(i) | $\text{Per}(X)$ is the D2921: Set of permutations on $X$ |

Then
\begin{equation}
|\text{Per}(X)| = |X|!
\end{equation}

Result R1851
on D15: Set cardinality

Cardinality of set of permutations on finite set

Formulation 0

Let $X$ be a D17: Finite set such that

(i) | $\text{Per}(X)$ is the D2921: Set of permutations on $X$ |

Then
\begin{equation}
|\text{Per}(X)| = |X|!
\end{equation}

Proofs

Let $X$ be a D17: Finite set such that

(i) | $\text{Per}(X)$ is the D2921: Set of permutations on $X$ |

Let $\text{Inj}(X \to X)$ be the D2222: Set of injections from $X$ to itself. Since $X$ is finite, result R1855: Conditions for endomorphism on finite set to qualify as permutation shows that $\text{Per}(X) = \text{Inj}(X \to X)$. Therefore, applying R1854: Cardinality of the set of injections between finite sets yields
\begin{equation}
|\text{Per}(X)| = |\text{Inj}(X \to X)| = \frac{|X|!}{(|X| - |X|)!} = |X|!
\end{equation}
$\square$