Proof of A Predicative Formula for Continuity at a Point, and the Set of Real-Valued Maps Continuous at a Point

Proof of (i). The formula. Let $\varepsilon$, $\delta$, $y$, $n$, $a$, $b$ and $m$ be distinct set variables, other than $g$, $s$ and the parameters. Let $\beta(s,y,\delta)$ be the formula

$$\exists n\,\bigl(((s,y),n)\in d\wedge n<\delta\bigr),$$

let $\kappa(g,s,y,\varepsilon)$ be the formula

$$\exists a\,\exists b\,\exists m\,\bigl((y,a)\in g\wedge(s,b)\in g\wedge((a,b),m)\in e\wedge m<\varepsilon\bigr),$$

and let $\Gamma(g,s)$ be the formula

$$\gamma(g,s)\wedge\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists\delta\,\bigl(\delta\in\mathbb{R}\wedge0<\delta\wedge\forall y\,((y\in S\wedge\beta(s,y,\delta))\Rightarrow\kappa(g,s,y,\varepsilon))\bigr)\Bigr).$$

Here $(y,a)\in g$ and $(s,b)\in g$ are the formulas of 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), $((s,y),n)\in d$ and $((a,b),m)\in e$ those of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), and $n<\delta$, $m<\varepsilon$, $0<\varepsilon$ and $0<\delta$ are, in the relation notation of Partial and Total Orders on a Set and the Associated Strict Relation (iii), memberships of ordered pairs in the parameter $<$, formulas of 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). The free variables of $\Gamma$ are among $g$, $s$ and the parameters.

Predicativity. $\gamma$ is predicative 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 (vii), the pair memberships 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 Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv). $\Gamma$ is built from these and from the memberships $\varepsilon\in\mathbb{R}$, $\delta\in\mathbb{R}$, $y\in S$ and $s\in S$ by connectives and by quantifiers over the set variables $\varepsilon$, $\delta$, $y$, $n$, $a$, $b$ and $m$ only. The subformulas $\gamma$ and the pair memberships, being predicative, contain no quantifier over a class variable. So no quantifier of $\Gamma$ is applied to a class variable, and $\Gamma$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Fix an assignment of sets to $g$ and $s$. If $\gamma(g,s)$ fails, then $\Gamma(g,s)$ fails by its first conjunct, and so does the condition. Let now $\gamma(g,s)$ hold: 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 (vii), $g:S\to Y$ is a map, and $s\in S$. By Metric Space (vi), $d:X\times X\to\mathbb{R}$ and $e:Y\times Y\to\mathbb{R}$ are maps. Let $\delta,\varepsilon\in\mathbb{R}$ and $y\in S$.

First, as $S\subseteq X$, $s,y\in X$, so $(s,y)\in X\times X$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). 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 (iv) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), for every set $n$, $((s,y),n)\in d$ holds if and only if $n=d(s,y)$, and $d(s,y)\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 $\beta(s,y,\delta)$ holds if and only if $d(s,y)<\delta$.

Second, 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 Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), for all sets $a$ and $b$, $(y,a)\in g$ holds if and only if $a=g(y)$, and $(s,b)\in g$ if and only if $b=g(s)$; and $g(y),g(s)\in Y$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $(g(y),g(s))\in Y\times Y$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). 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 (iv) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) for the map $e$, for every set $m$, $((g(y),g(s)),m)\in e$ holds if and only if $m=e(g(y),g(s))$. So the conjuncts of $\kappa(g,s,y,\varepsilon)$ before $m<\varepsilon$ hold exactly for $a=g(y)$, $b=g(s)$ and $m=e(g(y),g(s))$, and $\kappa(g,s,y,\varepsilon)$ holds if and only if $e(g(y),g(s))<\varepsilon$.

For a set $y\notin S$ the antecedent $y\in S\wedge\beta(s,y,\delta)$ fails. Hence $\Gamma(g,s)$ holds if and only if for every $\varepsilon\in\mathbb{R}$ with $0<\varepsilon$ there is $\delta\in\mathbb{R}$ with $0<\delta$ such that every $y\in S$ with $d(s,y)<\delta$ satisfies $e(g(y),g(s))<\varepsilon$, that is, by Continuous Map Between Metric Spaces (i) with $S$, $g$, $s$, $d$ and $e$ for $A$, $f$, $x$, $d_{X}$ and $d_{Y}$, if and only if $g$ is continuous at $s$ relative to $S$. So under every assignment, $\Gamma(g,s)$ holds if and only if $\gamma(g,s)$ holds and $g$ is continuous at $s$ relative to $S$: $\Gamma$ expresses this condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii), with $g$ and $s$ for $x_{1}$ and $x_{2}$.

Proof of (ii). By The Distance on the Real Numbers (i), $d_{\mathbb{R}}$ is a map $\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, and it is a metric on $\mathbb{R}$ by The Absolute Value Metric on the Real Numbers (i); so $(\mathbb{R},d_{\mathbb{R}})$ is a metric space by Metric Space (vi), and (i) applies to it: a predicative formula $\psi(g,s)$ expressing the condition there exists, for instance the formula $\Gamma$ above with $\mathbb{R}$ and $d_{\mathbb{R}}$ for $Y$ and $e$. Let $\psi$ be any such formula, and let $\psi(g,s_{0})$ be $\psi$ with a set variable $s_{0}$, other than $g$ and the variables of $\psi$, put for $s$ and given the value $s_{0}$; 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 (i) it is predicative, and for every set $g$ it holds if and only if $\psi(g,s)$ holds with $s_{0}$ assigned to $s$. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), $\mathbb{R}^{S}$ is a set; taking it as a further parameter, the class $C=\{g\in\mathbb{R}^{S}:\psi(g,s_{0})\}$ exists by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), and for every set $g$, $g\in C$ if and only if $g\in\mathbb{R}^{S}$ and $\psi(g,s_{0})$.

Let $g$ be a set. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $g\in\mathbb{R}^{S}$ if and only if $g$ is a map $g:S\to\mathbb{R}$. As $s_{0}\in S$, the guard $\gamma(g,s_{0})$ of (i) for $(\mathbb{R},d_{\mathbb{R}})$ then holds, so $\psi(g,s_{0})$ holds if and only if $g$ is continuous at $s_{0}$ relative to $S$. Hence $g\in C$ if and only if $g$ is a map $g:S\to\mathbb{R}$ continuous at $s_{0}$ relative to $S$. If $\psi'$ is another predicative formula expressing the same condition, then for every set $g$, $\psi'(g,s_{0})$ holds if and only if $\psi(g,s_{0})$ does, so the classes $\{g\in\mathbb{R}^{S}:\psi(g,s_{0})\}$ and $\{g\in\mathbb{R}^{S}:\psi'(g,s_{0})\}$ have the same elements and are equal by The Class Comprehension Theorem for Predicative Formulas (ii); this justifies the notation $C_{s_{0}}(S,d)=C$. Every element of $C$ lies in $\mathbb{R}^{S}$, so $C\subseteq\mathbb{R}^{S}$ by Subclasses and Subsets (i), and $C$ is 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).