Proof of Sections of a Sequence of Maps into a Metric Space, and the Map of Their Limits

Let $\phi:\mathbb{N}\to Y^{D}$ be the given sequence, so that $f_{k}=\phi(k)$ for every $k\in\mathbb{N}$ (Sequences (i)).

Proof of (i). Let $t\in D$. For $k\in\mathbb{N}$, $f_{k}\in Y^{D}$ is a map $f_{k}:D\to Y$ by The Class of All Functions from One Set to Another (i), so $f_{k}(t)\in Y$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). By Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), with $\mathbb{N}$ and $Y$ for its $A$ and $B$, $k$ for its $u$, $t$ for its $v_{1}$, the guard $t\in D$ for its $\gamma$, and the expression $\phi(k)(t)$ in $k$ and $t$, with $\phi$, $D$, $\mathbb{N}$ and $Y$ as parameters, the map $s_{t}:\mathbb{N}\to Y$, $k\mapsto f_{k}(t)$, exists and is the only set $h$ satisfying a predicative formula $\theta(h,t)$. By Sequences (i), $s_{t}$ is a sequence in $Y$ with $k$-th term $f_{k}(t)$, and every sequence in $Y$ with these terms equals $s_{t}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). So $s_{t}=(f_{k}(t))_{k\in\mathbb{N}}$, and $s_{t}$ is a defined set symbol in $t$, given by $\theta$ and used properly for $t\in D$: an expression in $t$ of the kind Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (v) takes.

Proof of (ii). By hypothesis, $s_{t}$ is convergent in $(Y,d_{Y})$ for every $t\in S$, and $S\subseteq D$; as $D$ is a set, $S$ 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). By Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (v), with $(Y,d_{Y})$ for its $(X,d)$, $S$ for its $a$ and the expression $s_{t}$ in $t$ for its $t(u)$, there is a map $f:S\to Y$ with $f(t)=\lim s_{t}$ for every $t\in S$, where $\lim s_{t}$ is the limit $\lim_{k\to\infty}f_{k}(t)$ of $s_{t}$ in $(Y,d_{Y})$ of The Limit of a Convergent Sequence in a Metric Space (i) (Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iii)). By The Limit of a Convergent Sequence in a Metric Space (ii), $s_{t}$ converges to $f(t)$ in $(Y,d_{Y})$ for every $t\in S$. This proves existence and the description of $f(t)$.

For uniqueness, let $f':S\to Y$ be a map such that $s_{t}$ converges to $f'(t)$ in $(Y,d_{Y})$ for every $t\in S$. For $t\in S$, $s_{t}$ converges to both $f(t)$ and $f'(t)$, so $f'(t)=f(t)$ by Uniqueness of Limits in a Metric Space (i). Hence $f'=f$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).