Proof of Kit for def:compact-space-and-subset

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},x_{1},x_{2}$ are distinct also when $n<3$. The parameters $\mathbb{N}_{0}$, $\mathbb{N}$ and the order of $\mathbb{N}_{0}$ are three distinct class variables, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). The letters $c$, $e$, $s$, $u$, $v$ and $w$ denote further set variables, distinct from one another and from $x_{0},x_{1},\dots$. The defined set symbols $\emptyset$, $\mathcal{P}$, $\bigcup$ and $\cap$ below are applied to sets only (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii)). Routine set bookkeeping is used without comment: elements of classes are sets (Classes, Membership, Sets and Proper Classes (i)), and so are subsets (Subclasses and Subsets (i)) and subclasses of sets (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)), in particular $u\cap v$ and $A\cap u$ below and a topology on a set $X$, a subset of $\mathcal{P}(X)$ (Topological Space); and a one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)).

Finiteness. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii), with $e$ as its set variable $A$ and the three parameters as its class variables, there is a predicative formula $\mathrm{fin}(e)$, with free variables among $e$ and the parameters, that holds for a set assigned to $e$ if and only if that set is finite; its bound variables are chosen other than the letters above.

Topological spaces. Write $X$ and $\mathcal{T}$ for $x_{0}$ and $x_{1}$, and let

$$\tau=\mathcal{T}\subseteq\mathcal{P}(X)\wedge\emptyset\in\mathcal{T}\wedge X\in\mathcal{T}\wedge\forall s\,\Bigl(s\subseteq\mathcal{T}\Rightarrow\bigcup s\in\mathcal{T}\Bigr)\wedge\forall u\,\forall v\,\bigl((u\in\mathcal{T}\wedge v\in\mathcal{T})\Rightarrow u\cap v\in\mathcal{T}\bigr).$$

It is predicative, no quantifier in it being applied to a class variable (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)), and its free variables are $x_{0}$ and $x_{1}$. Let sets $X$ and $\mathcal{T}$ be assigned to $x_{0}$ and $x_{1}$. The first conjunct of $\tau$ says that $\mathcal{T}$ is a subset of the power set $\mathcal{P}(X)$, the standing hypothesis of Topological Space, which "$(X,\mathcal{T})$ is a topological space" includes for arbitrary sets. The quantifier $\forall s$ ranges over sets (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)), so the fourth conjunct says that $\bigcup\mathcal{S}\in\mathcal{T}$ for every subset $\mathcal{S}$ of $\mathcal{T}$. Hence $\tau$ holds if and only if $\mathcal{T}\subseteq\mathcal{P}(X)$ and $\mathcal{T}$ satisfies Topological Space (ii), Topological Space (iii) and Topological Space (iv), that is, by Topological Space (i) and Topological Space (v), if and only if $(X,\mathcal{T})$ is a topological space.

The formula for compact spaces. Let

$$\kappa=\forall c\,\Bigl(\Bigl(c\subseteq\mathcal{T}\wedge X\subseteq\bigcup c\Bigr)\Rightarrow\exists e\,\Bigl(e\subseteq c\wedge\mathrm{fin}(e)\wedge X\subseteq\bigcup e\Bigr)\Bigr),\qquad\varphi=\tau\wedge\kappa.$$

The formula $\varphi$ is predicative, being built from abbreviations and the predicative formula $\mathrm{fin}$ by connectives and quantifiers over set variables only (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and its free variables are among $x_{0}$, $x_{1}$ and the parameters. Let sets $X$ and $\mathcal{T}$ be assigned to $x_{0}$ and $x_{1}$. If $(X,\mathcal{T})$ is not a topological space, then $\tau$ fails, and so do $\varphi$ and the condition of (i). Suppose that $(X,\mathcal{T})$ is a topological space, so that $\tau$ holds. As the quantifiers $\forall c$ and $\exists e$ range over sets, $\kappa$ says that for every subset $\mathcal{U}$ of $\mathcal{T}$ with $X\subseteq\bigcup\mathcal{U}$ there is a finite subset $\mathcal{V}$ of $\mathcal{U}$ with $X\subseteq\bigcup\mathcal{V}$, that is, by Compact Topological Space and Compact Subset (i), that $(X,\mathcal{T})$ is compact. In both cases $\varphi$ holds if and only if $(X,\mathcal{T})$ is a topological space and is compact. So $\varphi$ is a predicative formula in $x_{0},x_{1}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing this condition with $X=x_{0}$ and $\mathcal{T}=x_{1}$.

The formula for compact subsets. Write $A$ for $x_{2}$, and let

$$\omega=w\subseteq A\wedge\exists u\,(u\in\mathcal{T}\wedge w=A\cap u),$$ $$\lambda=\forall c\,\Bigl(\Bigl(\forall w\,(w\in c\Rightarrow\omega)\wedge A\subseteq\bigcup c\Bigr)\Rightarrow\exists e\,\Bigl(e\subseteq c\wedge\mathrm{fin}(e)\wedge A\subseteq\bigcup e\Bigr)\Bigr),\qquad\psi=\tau\wedge A\subseteq X\wedge\lambda.$$

As for $\varphi$, the formula $\psi$ is predicative, and its free variables are among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters. Let sets $X$, $\mathcal{T}$ and $A$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $(X,\mathcal{T})$ is not a topological space or $A\not\subseteq X$, then $\psi$ fails, and so does the condition of (ii). Suppose that $(X,\mathcal{T})$ is a topological space and $A\subseteq X$, and let $\mathcal{T}_{A}$ be the subspace topology on $A$. By Subspace Topology (i) and The Union Set and the Power Set of a Set (ii), a set $w$ lies in $\mathcal{T}_{A}$ if and only if

$$w\subseteq A\quad\text{and}\quad w=A\cap u\ \text{ for some }u\in\mathcal{T},$$

that is, if and only if $\omega$ holds; so, for a set $c$, the formula $\forall w\,(w\in c\Rightarrow\omega)$ holds if and only if $c\subseteq\mathcal{T}_{A}$ (Subclasses and Subsets (i)). As $\mathcal{T}_{A}$ is a subclass of the set $\mathcal{P}(A)$, it is a set; thus $\forall c$ ranges over all subsets of $\mathcal{T}_{A}$, and, as before, $\exists e$ over all subsets of $c$. Hence $\lambda$ holds if and only if for every subset $\mathcal{U}$ of $\mathcal{T}_{A}$ with $A\subseteq\bigcup\mathcal{U}$ there is a finite subset $\mathcal{V}$ of $\mathcal{U}$ with $A\subseteq\bigcup\mathcal{V}$, that is, by Compact Topological Space and Compact Subset (i) applied to the topological space $(A,\mathcal{T}_{A})$ (The Subspace Topology is a Topology (i)), if and only if $(A,\mathcal{T}_{A})$ is compact, which by Compact Topological Space and Compact Subset (ii) means that $A$ is compact in $(X,\mathcal{T})$. In all cases $\psi$ holds if and only if $(X,\mathcal{T})$ is a topological space, $A\subseteq X$ and $A$ is compact in $(X,\mathcal{T})$. So $\psi$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing this condition with $X=x_{0}$, $\mathcal{T}=x_{1}$ and $A=x_{2}$.

Compact spaces. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$ and $\sigma(0)=i$ and $\sigma(1)=j$, the formula $\varphi(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $(x_{i},x_{j})$ is a topological space and is compact. This proves (i).

Compact subsets. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=k$, the formula $\psi(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $(x_{i},x_{j})$ is a topological space, $x_{k}\subseteq x_{i}$ and $x_{k}$ is compact in $(x_{i},x_{j})$. This proves (ii).

The class of compact subsets. Let $(X,\mathcal{T})$ be a topological space; $X$ and $\mathcal{T}$ are sets. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\psi$ with its abbreviations eliminated, with $x_{2}$ as its single variable and $x_{0}$, $x_{1}$ and the three parameters as its parameters, $x_{0}$ and $x_{1}$ being assigned $X$ and $\mathcal{T}$. It gives a class $C$ whose elements are exactly the sets $A$ for which $\psi$ holds with $x_{0}$, $x_{1}$ and $x_{2}$ assigned $X$, $\mathcal{T}$ and $A$, that is, as $(X,\mathcal{T})$ is a topological space, the sets $A\subseteq X$ that are compact in $(X,\mathcal{T})$. This proves (iii).

The class of compact topologies. Let $X$ be a set. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi$ with its abbreviations eliminated, with $x_{1}$ as its single variable and $x_{0}$ and the three parameters as its parameters, $x_{0}$ being assigned $X$. It gives a class $S$ whose elements are exactly the sets $\mathcal{T}$ for which $\varphi$ holds with $x_{0}$ and $x_{1}$ assigned $X$ and $\mathcal{T}$, that is, those for which $(X,\mathcal{T})$ is a topological space and is compact. This proves (iv).