Kit for def:compact-space-and-subset

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$, not necessarily distinct. A condition on $x_{0},\dots,x_{n-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the set variables listed in Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}_{0}$, $\mathbb{N}$ and the order of $\mathbb{N}_{0}$ are parameters. Topological spaces are as in Topological Space (v), subsets as in Subclasses and Subsets (i), and compact spaces and compact subsets as in Compact Topological Space and Compact Subset (i) and Compact Topological Space and Compact Subset (ii). In the first clause $X=x_{i}$ and $\mathcal{T}=x_{j}$; in the second also $A=x_{k}$.

(i) Compact spaces. The condition "$(X,\mathcal{T})$ is a topological space and $(X,\mathcal{T})$ is compact" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Compact subsets. The condition "$(X,\mathcal{T})$ is a topological space, $A\subseteq X$, and $A$ is compact in $(X,\mathcal{T})$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) The class of compact subsets. For every topological space $(X,\mathcal{T})$ there is a class $C$ such that, for every class $A$, $A\in C$ if and only if $A\subseteq X$ and $A$ is compact in $(X,\mathcal{T})$.

(iv) The class of compact topologies. For every set $X$ there is a class $S$ such that, for every class $\mathcal{T}$, $\mathcal{T}\in S$ if and only if $(X,\mathcal{T})$ is a topological space and $(X,\mathcal{T})$ is compact.