Proof of The Invertible Matrices and the Positive Semidefinite Matrices Form Sets

Each result cited is universally quantified over the data in its own statement.

Tools. Formulas below are written with ordered pairs used as defined set symbols, which exist for all sets, and with sets and classes as parameters; no quantifier in them is applied to a class variable, so they are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. For a function $F$ and sets $c$ and $z$, $(c,z)\in F$ holds if and only if $c\in\operatorname{dom}F$ and $z=F(c)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value; for a map $F:U\to W$, $\operatorname{dom}F=U$ by Functions, Values of a Function, and Functions from One Class to Another §map. Classes given by such formulas are formed as in Sets and Maps: Ordinary Notation §set-builder, with elements as in Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction. Uniqueness in both clauses holds by Axiom of Extensionality for Classes: two sets with the elements described have the same elements.

Clause invertible. Let $\pi:\mathcal{M}_{n}(\mathbb{R})\times\mathcal{M}_{n}(\mathbb{R})\to\mathcal{M}_{n}(\mathbb{R})$ be the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique §product, with $n$ for each of its $m$, $n$ and $p$, so that $AB=\pi(A,B)$ for $A,B\in\mathcal{M}_{n}(\mathbb{R})$ by Product of Real Matrices §product; and let $I_{n}$ be the identity matrix. With the parameters $M=\mathcal{M}_{n}(\mathbb{R})$, $\pi$ and $E=I_{n}$, let $\varphi(A)$ be the formula

$$\exists B\,\bigl(B\in M\wedge((A,B),E)\in\pi\wedge((B,A),E)\in\pi\bigr),$$

predicative by the tools. Let $A\in\mathcal{M}_{n}(\mathbb{R})$. For every $B\in\mathcal{M}_{n}(\mathbb{R})$, the pairs $(A,B)$ and $(B,A)$ lie in $\mathcal{M}_{n}(\mathbb{R})\times\mathcal{M}_{n}(\mathbb{R})=\operatorname{dom}\pi$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, so by the tools $((A,B),E)\in\pi$ if and only if $AB=I_{n}$, and $((B,A),E)\in\pi$ if and only if $BA=I_{n}$. Hence $\varphi(A)$ holds if and only if there is $B\in\mathcal{M}_{n}(\mathbb{R})$ with $AB=I_{n}$ and $BA=I_{n}$, that is, by Inverse Matrix and Invertible Real Square Matrix §inverse, if and only if $A$ has an inverse, that is, by Inverse Matrix and Invertible Real Square Matrix §invertible, if and only if $A$ is invertible.

By Sets and Maps: Ordinary Notation §set-builder, $\mathrm{GL}_{n}(\mathbb{R})=\{A\in\mathcal{M}_{n}(\mathbb{R}):\varphi(A)\}$ is a set, $\mathcal{M}_{n}(\mathbb{R})$ being a set by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices; and for every set $A$, $A\in\mathrm{GL}_{n}(\mathbb{R})$ if and only if $A\in\mathcal{M}_{n}(\mathbb{R})$ and $\varphi(A)$, that is, if and only if $A\in\mathcal{M}_{n}(\mathbb{R})$ and $A$ is invertible. In particular every element of $\mathrm{GL}_{n}(\mathbb{R})$ lies in $\mathcal{M}_{n}(\mathbb{R})$, so it is a subset of $\mathcal{M}_{n}(\mathbb{R})$ by Subclasses and Subsets §subclass.

Clause psd. Let $\phi:\mathcal{M}_{n}(\mathbb{R})\times\mathbb{R}^{n}\to\mathbb{R}^{n}$ be the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique §matrix-vector, with $n$ for its $m$ and $n$, so that $Az=\phi(A,z)$ by Matrix-Vector Product §product; let $\delta:\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ be the map of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §dot-product, so that $\delta(z,w)=z\cdot w$, the dot product; and let $\le$ be the order of $\mathbb{R}$, a relation, so that $c\le q$ means $(c,q)\in{\le}$ by Relations, Domain, Range, Inverse and Composition §relation. With the parameters $R=\mathbb{R}^{n}$, $\phi$, $\delta$, $o=0\in\mathbb{R}$ and $L={\le}$, let $\psi(A)$ be the formula

$$\forall z\,\Bigl(z\in R\Rightarrow\exists w\,\exists q\,\bigl(((A,z),w)\in\phi\wedge((z,w),q)\in\delta\wedge(o,q)\in L\bigr)\Bigr),$$

predicative by the tools. Let $A\in\mathcal{S}(n)$; then $A\in\mathcal{M}_{n}(\mathbb{R})$ by Symmetric Real Matrices and the Set $\mathcal{S}(n)$ §set. Let $z\in\mathbb{R}^{n}$. As $(A,z)\in\operatorname{dom}\phi$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, the tools give: $((A,z),w)\in\phi$ if and only if $w=Az$; and $Az\in\mathbb{R}^{n}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph, so $(z,Az)\in\operatorname{dom}\delta$ and $((z,Az),q)\in\delta$ if and only if $q=z\cdot(Az)$. Hence the part $\exists w\,\exists q\,(\dots)$ holds for this $z$ if and only if $(0,z\cdot(Az))\in{\le}$, that is, $0\le z\cdot(Az)$. So $\psi(A)$ holds if and only if $z\cdot(Az)\ge0$ for every $z\in\mathbb{R}^{n}$, with $\ge$ as in Sets and Maps: Ordinary Notation §orders, that is, by Positive Semidefinite and Positive Definite Real Matrices §psd, if and only if $A$ is positive semidefinite.

$\mathcal{S}(n)$ is a set, a subset of the set $\mathcal{M}_{n}(\mathbb{R})$ by Symmetric Real Matrices and the Set $\mathcal{S}(n)$ §set. By Sets and Maps: Ordinary Notation §set-builder, $\mathcal{S}_{+}(n)=\{A\in\mathcal{S}(n):\psi(A)\}$ is a set, and for every set $A$, $A\in\mathcal{S}_{+}(n)$ if and only if $A\in\mathcal{S}(n)$ and $\psi(A)$, that is, if and only if $A\in\mathcal{S}(n)$ and $A$ is positive semidefinite. Every element of $\mathcal{S}_{+}(n)$ lies in $\mathcal{S}(n)$, so it is a subset of $\mathcal{S}(n)$ by Subclasses and Subsets §subclass.