Values of Variables and Set Parameters Are Sets; a Predicative Monotonicity Condition

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $x_{0},x_{1},\dots$ be distinct set variables. For a metatheoretic number $r\ge0$, a predicative formula in $x_{0},\dots,x_{r-1}$ is a predicative formula that expresses a condition on $x_{0},\dots,x_{r-1}$, with no displayed variables, as in Conditions Expressed by a Predicative Formula, and Guards (ii). There $x_{0},\dots,x_{r-1}$ take the place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i), whose parameters, fixed values and assignments are used throughout.

(i) Let $n\ge0$ be a metatheoretic number and let $\tau$ be a variable $x_{j}$ with $j<n$ or a parameter whose value is a set. Then under every assignment of sets to $x_{0},\dots,x_{n-1}$, whatever is assigned to the other variables $x_{n},x_{n+1},\dots$, the value of $\tau$ is a set.

(ii) Let $F$, $\mathbb{N}$, $\le_{\omega}$ and $\overline{\le}$ be distinct class variables, parameters whose fixed values are a class, also denoted $F$, and the set of natural numbers, the order on $\omega$ and the order on the extended real line. Then the condition on $x_{0}$

$$\text{for every set } m \text{ with } m\in\mathbb{N} \text{ and } (m,x_{0})\in{\le_{\omega}} \text{ there are sets } a \text{ and } b \text{ with } (m,a)\in F,\ (x_{0},b)\in F \text{ and } (a,b)\in{\overline{\le}},$$

where $(m,x_{0})$, $(m,a)$, $(x_{0},b)$ and $(a,b)$ are ordered pairs, is expressed by a predicative formula in $x_{0}$.