Proof of Kit for def:lebesgue-integral-nonnegative

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated; the given $x_{0},\dots,x_{N-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{3}$ are distinct also when $N<4$, and the bound variables of the cited formulas are chosen other than $x_{0},x_{1},\dots$ and the parameters; the earlier versions of the definitions on which The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions is stated give the same measurable spaces, measures, set $\mathcal{M}^{+}$ and integrals as the current ones (The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (v)); and routine facts about maps and sets are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii)).

The formula for measures on $(X,\mathcal{F})$. By Kit for def:measure-measure-space (ii), with its $n$ equal to $3$ and $i=0$, $j=1$, $k=2$, there is a predicative formula $\kappa$ in $x_{0},x_{1},x_{2}$ which, for sets $Y$, $\mathcal{G}$ and $m$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$, holds if and only if $(Y,\mathcal{G})$ is a measurable space and $m$ is a measure on $(Y,\mathcal{G})$. By Renaming and Substituting Variables in Predicative Formulas (iii), with its $k$ equal to $3$, its $n$ equal to $1$ and $\tau_{0}=X$, $\tau_{1}=\mathcal{F}$, $\tau_{2}=x_{0}$, the formula $\alpha=\kappa(X,\mathcal{F},x_{0})$ is a predicative formula in $x_{0}$. As $(X,\mathcal{F})$ is a measurable space, $\alpha$ holds for a set $\mu$ assigned to $x_{0}$ if and only if $\mu$ is a measure on $(X,\mathcal{F})$.

The formula for the integral. Let $\varphi$ be the predicative formula in $x_{0},x_{1},x_{2}$ given by The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (ii), with its $N$ equal to $3$ and $i=0$, $j=1$, $k=2$, for the measurable space $(X,\mathcal{F})$ fixed here. For sets $m'$, $g$ and $r$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$, $\varphi$ holds if and only if $m'$ is a map $m':\mathcal{F}\to[0,\infty]$, $g\in\mathcal{M}^{+}$ and $r=\int g\,dm'$, the integral being formed with $m'$ in place of the measure; when $m'$ is a measure on $(X,\mathcal{F})$, this is the integral of $g$ with respect to $m'$ of Nonnegative Measurable Maps and Their Lebesgue Integral (ii). By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$, its $n$ equal to $4$ and $\sigma(0)=0$, $\sigma(1)=2$, $\sigma(2)=3$, the formula $\varphi(x_{0},x_{2},x_{3})$ is a predicative formula in $x_{0},\dots,x_{3}$, which holds exactly when $x_{0}$ is a map $\mathcal{F}\to[0,\infty]$, $x_{2}\in\mathcal{M}^{+}$ and $x_{3}=\int x_{2}\,dx_{0}$.

For variables $F'$, $A$ and $B$, let $\mathrm{Map}(F',A,B)$ be the predicative formula 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 (vii) (called $\mu(F',A,B)$ there), which holds for classes exactly when $F'$ is a map $F':A\to B$; formulas $(u,v)\in s$ are 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 (iii). With $Z$ the parameter of Kit for def:measure-measure-space whose value is $[0,\infty]$, let

$$\beta=\alpha\wedge\mathrm{Map}(x_{1},\mathcal{M}^{+},Z)\wedge\forall x_{2}\,\forall x_{3}\,\bigl((x_{2},x_{3})\in x_{1}\Rightarrow\varphi(x_{0},x_{2},x_{3})\bigr).$$

$\beta$ is a conjunction of predicative formulas and of a quantification over the set variables $x_{2}$ and $x_{3}$ of a predicative formula, hence predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{0}$, $x_{1}$ and the parameters.

Let sets $\mu$ and $J$ be assigned to $x_{0}$ and $x_{1}$. Suppose that $\beta$ holds. Then $\mu$ is a measure on $(X,\mathcal{F})$, by the formula for measures, and $J$ is a map $J:\mathcal{M}^{+}\to[0,\infty]$. For each $f\in\mathcal{M}^{+}$, $(f,J(f))\in J$, so $\varphi(x_{0},x_{2},x_{3})$ holds with $\mu$, $f$ and $J(f)$ assigned to $x_{0}$, $x_{2}$ and $x_{3}$, which gives

$$J(f)=\int f\,d\mu .$$

So $J$ and the integral with respect to $\mu$ of Nonnegative Measurable Maps and Their Lebesgue Integral (ii) are maps $\mathcal{M}^{+}\to[0,\infty]$ with the same value at every $f\in\mathcal{M}^{+}$, and they are equal. Conversely, let $\mu$ be a measure on $(X,\mathcal{F})$ and $J$ the integral with respect to $\mu$. Then $\alpha$ holds, $J$ is a map $J:\mathcal{M}^{+}\to[0,\infty]$, and for every pair $(g,r)\in J$ we have $g\in\mathcal{M}^{+}$ and $r=J(g)=\int g\,d\mu$, while $\mu$ is a map $\mu:\mathcal{F}\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)); so $\varphi(x_{0},x_{2},x_{3})$ holds with $\mu$, $g$ and $r$ assigned to $x_{0}$, $x_{2}$ and $x_{3}$, and $\beta$ holds. Hence $\beta$ is a predicative formula in $x_{0},x_{1}$ expressing the condition of (i) with $\mu=x_{0}$ and $J=x_{1}$.

The integral as a map. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$, its $n$ equal to $N$ and $\sigma(0)=i$, $\sigma(1)=j$, the formula $\beta(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ that holds exactly when $x_{i}$ is a measure on $(X,\mathcal{F})$ and $x_{j}$ is the integral with respect to $x_{i}$. This proves (i).