Proof 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

Each result cited is universally quantified over the data in its own statement. The number $n\in\mathbb{N}$ and the matrix $A\in\mathcal{M}_{n}(\mathbb{R})$ are arbitrary, so every clause proved below holds for every $n\in\mathbb{N}$ and every $A\in\mathcal{M}_{n}(\mathbb{R})$.

Preliminaries. For $q\in\mathbb{N}$, the elements of $\mathcal{M}_{q}(\mathbb{R})$ are the maps $[q]\times[q]\to\mathbb{R}$, with $B_{ij}=B((i,j))$, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries; the elements of $\mathbb{R}^{n}$ are the maps $u:[n]\to\mathbb{R}$, with $u_{j}=u(j)$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §space and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership; and the elements of $S_{n}$ are the bijections $[n]\to[n]$, by Permutations of a Set and the Set of Permutations of [n] §membership. Every map and every matrix formed below is given by an expression in its values or entries, which lie in the stated target, so it exists and is the only map with these values, as in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices §maps and Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices §predicativity.

Clause terms. Let $\sigma\in S_{n}$. For $i\in[n]$, $\sigma(i)\in[n]$, so $i\mapsto A_{i\sigma(i)}$ is a map $[n]\to\mathbb{R}$, and its product over the finite set $[n]$ lies in $\mathbb{R}$. Hence $t_{A}:S_{n}\to\mathbb{R}$, $\sigma\mapsto\operatorname{sgn}(\sigma)\prod_{i\in[n]}A_{i\sigma(i)}$, is a map, and the only one with these values.

Clause determinant. For $B\in\mathcal{M}_{n}(\mathbb{R})$, $t_{B}$ is the only map with the values of clause terms with $B$ in place of $A$, and $\sum_{\sigma\in S_{n}}t_{B}(\sigma)\in\mathbb{R}$ is its sum over the finite set $S_{n}$. Hence $D_{n}:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$, $B\mapsto\sum_{\sigma\in S_{n}}t_{B}(\sigma)$, is a map, and the only one with these values. Since $n\in\mathbb{N}$ was arbitrary, this clause holds with every element of $\mathbb{N}$ in place of $n$.

Clause row-reindexing. Let $f:[n]\to[n]$. For $i,j\in[n]$, $f(i)\in[n]$, so $(i,j)\mapsto A_{f(i)j}$ is a map $[n]\times[n]\to\mathbb{R}$, that is an element $A^{f}$ of $\mathcal{M}_{n}(\mathbb{R})$, and the only one with these entries.

Clause row-replacement. Let $i\in[n]$ and $u\in\mathbb{R}^{n}$. By Maps Defined by Cases §cases, with the sets $[n]\times[n]$ and $\mathbb{R}$, the property that the first component of $z=(k,j)$ is $i$, and the expressions $u_{j}$ and $A_{kj}$, there is exactly one $C\in\mathcal{M}_{n}(\mathbb{R})$ with $C_{ij}=u_{j}$ for all $j\in[n]$ and $C_{kj}=A_{kj}$ for all $j,k\in[n]$ with $k\neq i$. This $C$ is $A[i\leftarrow u]$.

Clause deletion. Let $2\le n$. Then $1\in[n]$, so $n-1\in\mathbb{N}$ by The Index Map Skipping One Element of [n] §difference applied with $i=1$. For $i\in[n]$, $s_{i}:[n-1]\to[n]$ is a map by The Deletion Index Map §deletion-index. Let $i,j\in[n]$. For $k,l\in[n-1]$, $(s_{i}(k),s_{j}(l))\in[n]\times[n]$, so $(k,l)\mapsto A_{s_{i}(k)s_{j}(l)}$ is a map $[n-1]\times[n-1]\to\mathbb{R}$, that is an element $A^{(i,j)}$ of $\mathcal{M}_{n-1}(\mathbb{R})$, and the only one with these entries.

Clause adjugate. Let $2\le n$, so that $n-1\in\mathbb{N}$ as in clause deletion, and $D_{n-1}:\mathcal{M}_{n-1}(\mathbb{R})\to\mathbb{R}$ is the map of clause determinant with $n-1$ in place of $n$. For $i,j\in[n]$, $A^{(j,i)}$ is, by clause deletion, the only element of $\mathcal{M}_{n-1}(\mathbb{R})$ with the entries given there, so $D_{n-1}(A^{(j,i)})\in\mathbb{R}$, and $(-1)^{j+i}\in\mathbb{R}$ with $j+i\in\mathbb{N}_{0}$. Hence $(i,j)\mapsto(-1)^{j+i}D_{n-1}(A^{(j,i)})$ is a map $[n]\times[n]\to\mathbb{R}$, that is an element $B$ of $\mathcal{M}_{n}(\mathbb{R})$, and the only one with these entries.