Proof of Permutations of [n] are Maps [n] → [n], and Values of the Determinant are Real Numbers

Let $n\in\mathbb{N}$. Then $n\in\mathbb{N}_{0}$, by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n §naturals, and Permutations of a Set and the Set of Permutations of [n] applies to $n$.

Clause permutation-map. Let $\sigma\in S_{n}$. Since $\sigma$ is an element of the class $S_{n}$, $\sigma$ is a set by Classes, Membership, Sets and Proper Classes §set. Hence Permutations of a Set and the Set of Permutations of [n] §membership applies to $u=\sigma$ and gives that $\sigma$ is a bijection $\sigma:[n]\to[n]$. By Injective, Surjective and Bijective Functions between Classes §bijective, bijectivity is defined for a map $F:A\to B$ between classes, in the sense of Functions, Values of a Function, and Functions from One Class to Another §map; so a bijection from $[n]$ to $[n]$ is in particular a map from $[n]$ to $[n]$, and $\sigma:[n]\to[n]$ is a map.

Clause determinant-value. Let $A\in\mathcal{M}_{n}(\mathbb{R})$. By Determinant of a Real Square Matrix §determinant, $\det:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$ is the map $D_{n}$ of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique §determinant, and $\det A$ is its value $D_{n}(A)$ at $A$. So Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph, applied to the map $D_{n}:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$ between the sets $\mathcal{M}_{n}(\mathbb{R})$ and $\mathbb{R}$ (Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, The Real Numbers §reals) and the point $A\in\mathcal{M}_{n}(\mathbb{R})$, gives $D_{n}(A)\in\mathbb{R}$, that is, $\det A\in\mathbb{R}$.