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

Terms under $\gamma$, their values and terms of a type are as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii); throughout, the parameters have their fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i). $\mathbb{R}$ is a set and $\le$ is a total order on it, by The Real Numbers (i), and $<$ is its strict relation.

Proof of (i). By Intervals of the Real Line (ii) and Intervals of the Real Line (iii), for $a,b\in\mathbb{R}$ the set $I(a,b)$ is $\{w\in\mathbb{R}:\beta(a,w,b)\}$, where $\beta(a,w,b)$ is, according to the form of $I$, one of $a\le w\wedge w\le b$, $a<w\wedge w<b$, $a\le w\wedge w<b$, $a<w\wedge w\le b$, $a<w$, $a\le w$, $w<b$ and $w\le b$. Let $z$, $a$ and $b$ be distinct set variables other than $Y$ and $L$, and let $w$ be a set variable that is none of $z$, $a$, $b$, $Y$ and $L$. Let $\beta'(a,w,b)$ be $\beta(a,w,b)$ with each part $p\le q$ written $(p,q)\in L$ and each part $p<q$ written $((p,q)\in L\wedge\neg\,p=q)$. By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (ii), for all $a,w,b\in\mathbb{R}$, $\beta'(a,w,b)$ holds if and only if $\beta(a,w,b)$ does. Let $\theta(z,a,b)$ be the formula $\forall w\,(w\in z\Leftrightarrow(w\in Y\wedge\beta'(a,w,b)))$. It applies no quantifier to a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and its free variables are among $z$, $a$, $b$, $Y$ and $L$. Let $a,b\in\mathbb{R}$. The class $\{w\in\mathbb{R}:\beta'(a,w,b)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii) is a subclass of $\mathbb{R}$, hence a set by 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), and it satisfies $\theta$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i); two sets satisfying $\theta$ have the same elements, so they are equal by Axiom of Extensionality for Classes. So exactly one set $z$ satisfies $\theta(z,a,b)$. Its elements are the $w\in\mathbb{R}$ with $\beta'(a,w,b)$, that is, with $\beta(a,w,b)$, so it is $I(a,b)$ by Axiom of Extensionality for Classes; it is a subset of $\mathbb{R}$, so it lies in $\mathcal{P}(\mathbb{R})$ by The Union Set and the Power Set of a Set (ii). By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii), $I(a,b)$ is therefore a defined set symbol given by $\theta$, used properly wherever $a,b\in\mathbb{R}$.

Proof of (ii). Values. Under an assignment satisfying $\gamma$, the values $a$ of $s$ and $b$ of $t$ lie in $\mathbb{R}$ by Terms and Typed Terms under a Guard (iii), so the value $I(a,b)$ of $I(s,t)$ is a set in $\mathcal{P}(\mathbb{R})$ by (i), determined by $a$, $b$ and the values of the parameters. So $I(s,t)$ is a term under $\gamma$ satisfying Terms and Typed Terms under a Guard (iii) with $\mathcal{P}(\mathbb{R})$.

The formula. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $I(s,t)$; as $Y$ and $L$ occur in $I(s,t)$, $z$ is neither of them. The set variables form an infinite list by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i), so there are distinct set variables $u$ and $v$ that are none of $x_{1},\dots,x_{k}$ and $z$ and occur neither in $\gamma$ nor in $I(s,t)$; in particular they are not $Y$ or $L$, and they do not occur in $s$ or $t$. By (i), applied to the distinct set variables $z$, $u$ and $v$, there is a predicative formula $\theta(z,u,v)$, with free variables among $z$, $u$, $v$, $Y$ and $L$, such that for all $u,v\in\mathbb{R}$ the only set $z$ satisfying $\theta(z,u,v)$ is $I(u,v)$. By Terms and Typed Terms under a Guard (iv) there are predicative formulas $\psi_{s}^{u}$ and $\psi_{t}^{v}$ expressing $\gamma\wedge u=s$ and $\gamma\wedge v=t$. By Conditions Expressed by a Predicative Formula, and Guards (ii), the free variables of $\psi_{s}^{u}$ are among $x_{1},\dots,x_{k}$, $u$ and the parameters of $\gamma$ and $s$, and those of $\psi_{t}^{v}$ among $x_{1},\dots,x_{k}$, $v$ and the parameters of $\gamma$ and $t$; so $z$ is free in neither, $v$ is not free in $\psi_{s}^{u}$, and $u$ is not free in $\psi_{t}^{v}$. Let $\psi$ be the formula $\exists u\,\exists v\,(\psi_{s}^{u}\wedge\psi_{t}^{v}\wedge\theta(z,u,v))$. It applies no quantifier to a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $I(s,t)$. Consider an assignment of sets to $x_{1},\dots,x_{k}$ and $z$. Since $v$ is not free in $\psi_{s}^{u}$, $\psi_{s}^{u}$ holds for sets assigned to $u$ and $v$ if and only if $\gamma$ holds and $u$ is the value $a$ of $s$; likewise, since $u$ is not free in $\psi_{t}^{v}$, $\psi_{t}^{v}$ holds if and only if $\gamma$ holds and $v$ is the value $b$ of $t$. So $\psi$ holds if and only if $\gamma$ holds and $\theta(z,a,b)$, where $a,b\in\mathbb{R}$ when $\gamma$ holds; that is, if and only if $\gamma$ holds and $z=I(a,b)$. So $\psi$ expresses $\gamma\wedge z=I(s,t)$, Terms and Typed Terms under a Guard (iv) holds, and $I(s,t)$ is of type $\mathcal{P}(\mathbb{R})$ by Terms and Typed Terms under a Guard (ii).

Proof of (iii). $\mathcal{P}(\mathbb{R})$ is a set by The Union Set and the Power Set of a Set (ii). For $i\in D$, $s_{i}$ and $t_{i}$ are values of maps at an element of their domain, defined set symbols used properly by Functions, Values of a Function, and Functions from One Class to Another (ii), and they lie in $\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii); so by (i) the expression $I(s_{i},t_{i})$ is built from defined set symbols used properly and lies in $\mathcal{P}(\mathbb{R})$. So Maps and Relations Given by Formulas (i), with $a=D$, $b=\mathcal{P}(\mathbb{R})$ and the expression $I(s_{u},t_{u})$ for $t(u)$, gives exactly one map $f$ as stated.