Proof of The Set of Indices n for Which the n-th Map of a Sequence in ℝ^[a,b] Is Integrable with a Prescribed Integral

The formula. The closed interval $[a,b]$ is a subset of $\mathbb{R}$ by Intervals of the Real Line (ii). Let $\Omega(g,u,v,z)$ be a predicative formula expressing the condition of A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) for $E=[a,b]$, with the parameters listed there. Let $\phi:\mathbb{N}\to\mathbb{R}^{[a,b]}$ and $\zeta:\mathbb{N}\to\mathbb{R}$ be the given sequences, so that $\phi(n)=h_{n}$ and $\zeta(n)=z_{n}$ for $n\in\mathbb{N}$ (Sequences (i)); $a$, $b$, $\phi$ and $\zeta$ are taken as further parameters with these values. Let $n$, $h$ and $w$ be set variables distinct from each other and from the parameters, and let $\Omega(h,a,b,w)$ be the formula obtained from $\Omega$ by putting $h$, $a$, $b$ and $w$ for $g$, $u$, $v$ and $z$, 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). Let

$$\chi(n):\quad n\in\mathbb{N}\wedge\exists h\,\exists w\,\bigl((n,h)\in\phi\wedge(n,w)\in\zeta\wedge\Omega(h,a,b,w)\bigr),$$

with $(n,h)\in\phi$ and $(n,w)\in\zeta$ 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). The free variables of $\chi$ are among $n$ and the parameters of the condition.

Predicativity. $\Omega(h,a,b,w)$ is predicative by A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) 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 (i), and 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). $\chi$ is built from them and a membership by connectives and by quantifiers over set variables only, so no quantifier in it is applied to a class variable, and $\chi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Let $m$ be a set. If $m\notin\mathbb{N}$, both $\chi(m)$ and the condition fail. Let $m\in\mathbb{N}$. Since $\phi$ is a map $\phi:\mathbb{N}\to\mathbb{R}^{[a,b]}$ with $\phi(m)=h_{m}$, Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) gives, for every set $h$, that $(m,h)\in\phi$ if and only if $h=h_{m}$; likewise $(m,w)\in\zeta$ if and only if $w=z_{m}$. Hence $\chi(m)$ holds if and only if $\Omega(h_{m},a,b,z_{m})$ holds, that is, 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) and A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i), if and only if $h_{m}$ is a map $h_{m}:[a,b]\to\mathbb{R}$, $a,b\in[a,b]$, $\int_{a}^{b}h_{m}$ is defined in the sense of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), and $z_{m}=\int_{a}^{b}h_{m}$. The first two of these hold: $h_{m}\in\mathbb{R}^{[a,b]}$ is a map from $[a,b]$ to $\mathbb{R}$ by Sets and Maps: Ordinary Notation (v), and $a,b\in[a,b]$ by Intervals of the Real Line (ii), as $a\le a\le b$ and $a\le b\le b$. Since $a<b$, neither $a=b$ nor $b<a$ holds: $a=b$ would give $a<a$, and $b<a$ would give $a<a$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iv), both contrary to Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iii); and $[a,b]\subseteq[a,b]$; so, by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), $\int_{a}^{b}h_{m}$ is defined if and only if $h_{m}$ is integrable on $[a,b]$ in the sense of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), and then $\int_{a}^{b}h_{m}$ is the number given there. By The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), this means that the restriction $h_{m}|_{[a,b]}$ is bounded and integrable on $[a,b]$, with $\int_{a}^{b}h_{m}=\int_{a}^{b}h_{m}|_{[a,b]}$; and $h_{m}|_{[a,b]}=h_{m}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii). So $\chi(m)$ holds if and only if $h_{m}$ is bounded and integrable on $[a,b]$ in the sense of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iv) and $z_{m}$ is its integral $\int_{a}^{b}h_{m}$ of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (v). Thus $\chi$ expresses the condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii).

Proof of (i). Let $\psi(n)$ be any predicative formula expressing the condition, for instance $\chi$. $\mathbb{N}$ is a set by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), so the class $\{n\in\mathbb{N}:\psi(n)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii) is a set by Sets and Maps: Ordinary Notation (iii). By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii), for every set $m$, $m\in\{n\in\mathbb{N}:\psi(n)\}$ if and only if $m\in\mathbb{N}$ and $\psi(m)$, that is, as $\psi$ expresses the condition, if and only if $m\in\mathbb{N}$, $h_{m}$ is bounded and integrable on $[a,b]$ and $\int_{a}^{b}h_{m}=z_{m}$. In particular every element of this set lies in $\mathbb{N}$, so it is a subset of $\mathbb{N}$ (Subclasses and Subsets (i)). Two such sets, formed from two formulas expressing the condition, have the same elements, so they are equal by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii); hence $A$ does not depend on the choice of the formula.