Proof of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits

Each result cited is universally quantified over the data in its own statement.

Clause converges. Predicativity. Write $\mu(s,\mathbb{N},X)$ out as the formula $\mu(F,A,B)$ 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 §map with $s$, $\mathbb{N}$ and $X$ put for $F$, $A$ and $B$; its quantifiers are over set variables only. The remaining quantifiers $\forall\varepsilon$, $\exists N$ and $\forall m$ of $\kappa$ are over set variables. The abbreviations written in $\kappa$ are the ordered pair, the values $s(m)$ and $d(s(m),z)=d((s(m),z))$ of Sets and Maps: Ordinary Notation §maps, which are defined set symbols by Functions, Values of a Function, and Functions from One Class to Another §value, and the relation notation $N\le m$, $0<\varepsilon$ and $d(s(m),z)<\varepsilon$, which stands for membership of an ordered pair in the parameter $\le$ or $<$ by Relations, Domain, Range, Inverse and Composition §relation; no class abstraction is written in $\kappa$. So no quantifier of $\kappa$ is applied to a class variable, and $\kappa$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Meaning. Let $s$ and $z$ be sets. 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 §map, $\mu(s,\mathbb{N},X)$ holds if and only if $s$ is a map $s:\mathbb{N}\to X$, that is, by Sequences §sequence, a sequence in $X$. If $s$ is not a sequence in $X$ or $z\notin X$, then $\kappa(s,z)$ fails by its first two conjuncts, and so does the right-hand side of the claim. Let now $s$ be a sequence in $X$ and $z\in X$. By Metric Space, $d$ is a map $d:X\times X\to\mathbb{R}$. For $m\in\mathbb{N}$, the value $s(m)$ is used properly, since $\operatorname{dom}s=\mathbb{N}$ by Functions, Values of a Function, and Functions from One Class to Another §map; $s(m)\in X$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph; hence $(s(m),z)\in X\times X=\operatorname{dom}d$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and Functions, Values of a Function, and Functions from One Class to Another §map, so $d((s(m),z))$ is used properly as well, and $d(s(m),z)\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph. These places of use lie under the left conjuncts $\mu(s,\mathbb{N},X)\wedge z\in X$ and the antecedent $m\in\mathbb{N}\wedge N\le m$, as Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols requires. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, applied in turn to the values $s(m)$ and $d(s(m),z)$, each used properly there, and 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 §pair-membership for the ordered pairs, the part $d(s(m),z)<\varepsilon$ holds if and only if the real number $d(s(m),z)$ is less than $\varepsilon$ in $\mathbb{R}$. So the third conjunct of $\kappa(s,z)$ states that for every $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$ there is $N\in\mathbb{N}$ with $d(s(m),z)<\varepsilon$ for every $m\in\mathbb{N}$ with $m\ge N$, where for $N,m\in\mathbb{N}$ the order of $\mathbb{R}$ agrees with that of $\mathbb{N}_{0}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §agreement. By Convergent Sequence in a Metric Space §converges, this is the statement that $s$ converges to $z$ in $(X,d)$.

Clause convergent. The formula $\gamma(s)$, that is $\exists z\,\kappa(s,z)$, is built from $\kappa$ by a quantifier over the set variable $z$; as no quantifier of $\kappa$ is applied to a class variable, neither is any quantifier of $\gamma$, and $\gamma$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. By the clause converges, for every set $s$ it holds if and only if $s$ is a sequence in $X$ and $s$ converges in $(X,d)$ to some $z\in X$, which by Convergent Sequence in a Metric Space §convergent is the statement that $s$ is convergent in $(X,d)$.

Clause limit-symbol. Predicativity. $\kappa$ is predicative by the clause converges. The formula $\kappa(s,z')$ is $\kappa(s,z)$ with the set variable $z'$, which does not occur in $\kappa$, put for $z$, so it has the same quantifiers as $\kappa$; and $\upsilon(s)$ and $\gamma'(s)$ are built from $\kappa(s,z)$, $\kappa(s,z')$, $\gamma(s)$ and the formula $z=z'$ by connectives and quantifiers over the set variables $z$ and $z'$. As no quantifier of $\kappa$ is applied to a class variable, neither is any quantifier of $\gamma'(s)$, and $\gamma'(s)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Uniqueness. Fix any values of the parameters, and let $s$ be a set with $\gamma'(s)$. By $\gamma(s)$, some set $z$ satisfies $\kappa(s,z)$; by $\upsilon(s)$, any sets $z$ and $z'$ with $\kappa(s,z)$ and $\kappa(s,z')$ are equal. So exactly one set $z$ satisfies $\kappa(s,z)$.

The metric space $(X,d)$. Let $s$ be a set, and let $z$ and $z'$ be sets with $\kappa(s,z)$ and $\kappa(s,z')$. By the clause converges, $s$ is a sequence in $X$, $z,z'\in X$, and $s$ converges to $z$ and to $z'$ in $(X,d)$; so $z=z'$ by Uniqueness of Limits in a Metric Space §unique. Hence $\upsilon(s)$ holds, and $\gamma'(s)$ holds if and only if $\gamma(s)$. Let now $\gamma(s)$ hold, so that $s$ is a convergent sequence in $X$ by the clause convergent. By The Limit of a Convergent Sequence in a Metric Space §limit and The Limit of a Convergent Sequence in a Metric Space §converges-to-limit, $\lim_{m\to\infty}s_{m}$ is a point of $X$ to which $s$ converges, so $\kappa(s,\lim_{m\to\infty}s_{m})$ holds by the clause converges, and $\lim s=\lim_{m\to\infty}s_{m}$ is the set $z$ with $\kappa(s,z)$.

The defined set symbol. By the above, $\kappa$ and $\gamma'$ are predicative and, for all values of the parameters and all sets $s$ satisfying $\gamma'(s)$, exactly one set $z$ satisfies $\kappa(s,z)$; these are the hypotheses of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination with $k=1$, $s$ for $v_{1}$, $\kappa$ for $\theta$ and $\gamma'$ for $\gamma$. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, $\lim s$ is then the defined set symbol with argument $s$ given by the predicative $\kappa$, and it is used properly where $\gamma(s)$ holds, since there exactly one set satisfies $\kappa(s,z)$.

Clause real. By The Distance on the Real Numbers §distance, $d_{\mathbb{R}}$ is a map $d_{\mathbb{R}}:\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 §metric; so $(\mathbb{R},d_{\mathbb{R}})$ is a metric space by Metric Space §metric-space, and the clauses above apply to it. By the clause converges for $(\mathbb{R},d_{\mathbb{R}})$, $\kappa(s,z)$ holds if and only if $s$ is a sequence in $\mathbb{R}$, $z\in\mathbb{R}$ and $s$ converges to $z$ in $(\mathbb{R},d_{\mathbb{R}})$, and by Convergence, Limits and the Cauchy Condition for Real Sequences Agree with Those in the Real Line as a Metric Space, which is Complete §converges the last condition is equivalent to $s$ converging to $z$ in the sense of Convergent Sequences of Real Numbers §converges. Let now $\kappa(s,z)$ hold. Then $\gamma(s)$ holds, so $z=\lim s$ by the clause limit-symbol for $(\mathbb{R},d_{\mathbb{R}})$. Further, $s$ converges to $z$ in the sense of Convergent Sequences of Real Numbers §converges, so it is convergent in that sense, and its limit $\lim_{n\to\infty}s_{n}$ of The Limit of a Convergent Sequence §limit is $z=\lim s$.

Clause maps. Suppose that $t(u)$ is a convergent sequence in $X$ for every $u\in a$. By the clause limit-symbol, the limit $\lim s$ is a defined set symbol with argument $s$, given by the predicative $\kappa$ and used properly where $\gamma(s)$ holds, that is, by the clause convergent, where $s$ is a convergent sequence in $X$; so in the expression $\lim t(u)$, obtained by putting $t(u)$ for its argument, every defined set symbol is used properly for every $u\in a$, and $\lim t(u)\in X$ by The Limit of a Convergent Sequence in a Metric Space §limit. Hence Maps and Relations Given by Formulas §map, applied to the sets $a$ and $X$ and this expression, gives exactly one map $f:a\to X$ with $f(u)=\lim t(u)$ for every $u\in a$.