Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps

This helper adopts the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; (i) and (ii) are statements of the metatheory about expressions. $\mathcal{P}(\mathbb{R})$ is the power set of $\mathbb{R}$. For $a,b\in\mathbb{R}$, let $I(a,b)$ be one fixed one of the eight forms $[a,b]$, $(a,b)$, $[a,b)$, $(a,b]$ of Intervals of the Real Line (ii) and $(a,\infty)$, $[a,\infty)$, $(-\infty,b)$, $(-\infty,b]$ of Intervals of the Real Line (iii), the same form for all $a$ and $b$. Let $Y$ and $L$ be distinct variables whose values are $\mathbb{R}$ and its order $\le$.

(i) For all distinct set variables $z$, $a$ and $b$ other than $Y$ and $L$, there is a predicative formula $\theta(z,a,b)$, whose free variables are among $z$, $a$, $b$, $Y$ and $L$, such that for all $a,b\in\mathbb{R}$ exactly one set $z$ satisfies $\theta(z,a,b)$, namely $I(a,b)$, and $I(a,b)\in\mathcal{P}(\mathbb{R})$. Thus $I(a,b)$ is a defined set symbol with the set arguments $a$ and $b$, given by $\theta$, used properly at all $a,b\in\mathbb{R}$, with values in $\mathcal{P}(\mathbb{R})$.

(ii) Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, none of them $Y$ or $L$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, and terms of type $A$ under $\gamma$ for a class $A$, be as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii). Let $s$ and $t$ be terms of type $\mathbb{R}$ under $\gamma$, and let $I(s,t)$ be the term under $\gamma$, written with $s$, $t$ and the parameters $Y$ and $L$, whose value under each assignment satisfying $\gamma$ is $I(a,b)$ for the values $a$ of $s$ and $b$ of $t$. Then $I(s,t)$ is a term of type $\mathcal{P}(\mathbb{R})$ under $\gamma$.

(iii) Let $D$ be a set and let $s,t:D\to\mathbb{R}$, $i\mapsto s_{i}$ and $i\mapsto t_{i}$, be maps. Then there is exactly one map $f:D\to\mathcal{P}(\mathbb{R})$ with $f(i)=I(s_{i},t_{i})$ for every $i\in D$.