Proof of Kit for def:lebesgue-integral-integrable

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, sets $\mathcal{L}^{1}(\mu)$ 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 (vi)); 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 (iii), 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$, $f$ 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]$, $f\in\mathcal{L}^{1}(m)$ and $r=\int f\,dm$, these being formed with $m$ in place of the measure. When $m$ is a measure $\mu$ on $(X,\mathcal{F})$, $(X,\mathcal{F},\mu)$ is a measure space, $\mathcal{L}^{1}(\mu)$ and $\int f\,d\mu$ are those of Integrable Functions and Their Lebesgue Integral (ii) and Integrable Functions and Their Lebesgue Integral (iii), and $\mu$ is a map $\mu:\mathcal{F}\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)). So, for a measure $\mu$ on $(X,\mathcal{F})$ and sets $f$ and $r$,

$$\varphi\ \text{holds with}\ \mu,f,r\ \text{assigned to}\ x_{0},x_{1},x_{2}\quad\Longleftrightarrow\quad f\in\mathcal{L}^{1}(\mu)\ \text{and}\ r=\int f\,d\mu .\tag{$*$}$$

Integrable functions. Let

$$\delta=\alpha\wedge\exists x_{2}\,\varphi .$$

It is a conjunction of a predicative formula and of a quantification over the set variable $x_{2}$ 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 $f$ be assigned to $x_{0}$ and $x_{1}$. If $\delta$ holds, then $\mu$ is a measure on $(X,\mathcal{F})$ and $\varphi$ holds with $\mu$, $f$ and some set $r$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$, so $f\in\mathcal{L}^{1}(\mu)$ by $(*)$. Conversely, if $\mu$ is a measure on $(X,\mathcal{F})$ and $f\in\mathcal{L}^{1}(\mu)$, then $\int f\,d\mu$ is a real number (Integrable Functions and Their Lebesgue Integral (iii)), hence a set, and $\varphi$ holds with $\mu$, $f$ and $\int f\,d\mu$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$ by $(*)$; so $\delta$ holds. Hence $\delta$ is a predicative formula in $x_{0},x_{1}$ expressing the condition of (i) with $\mu=x_{0}$ and $f=x_{1}$. 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 $\delta(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing this condition with $\mu=x_{i}$ and $f=x_{j}$. This proves (i).

The integral as a map. 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 $\varphi$ holds with the sets assigned to $x_{0}$, $x_{2}$ and $x_{3}$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$. For a variable $G$, let $\Phi(G)$ 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 (vi), which holds for a class $G$ exactly when $G$ is a function; 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). Let

$$\begin{aligned} \beta={}&\alpha\wedge\Phi(x_{1})\wedge\forall x_{2}\,\forall x_{3}\,\bigl((x_{2},x_{3})\in x_{1}\Rightarrow\varphi(x_{0},x_{2},x_{3})\bigr)\\ &\wedge\forall x_{2}\,\bigl(\exists x_{3}\,\varphi(x_{0},x_{2},x_{3})\Rightarrow\exists x_{3}\,(x_{2},x_{3})\in x_{1}\bigr). \end{aligned}$$

Every quantifier of $\beta$ is over a set variable and its other parts are predicative, so $\beta$ is predicative, with free variables among $x_{0}$, $x_{1}$ and the parameters.

Let sets $\mu$ and $I$ be assigned to $x_{0}$ and $x_{1}$. Suppose that $\beta$ holds. Then $\mu$ is a measure on $(X,\mathcal{F})$ and $I$ is a function. By the third conjunct and $(*)$, every pair $(f,r)\in I$ has $f\in\mathcal{L}^{1}(\mu)$ and $r=\int f\,d\mu$. For $f\in\mathcal{L}^{1}(\mu)$, $\varphi$ holds with $\mu$, $f$ and the set $\int f\,d\mu$ by $(*)$, so by the last conjunct $f$ is in the domain of $I$. So $I$ is a function with domain $\mathcal{L}^{1}(\mu)$ and

$$I(f)=\int f\,d\mu\in\mathbb{R}\qquad\text{for every}\ f\in\mathcal{L}^{1}(\mu);$$

thus $I$ and the integral with respect to $\mu$ of Integrable Functions and Their Lebesgue Integral (iii) are maps $\mathcal{L}^{1}(\mu)\to\mathbb{R}$ with the same value at every $f\in\mathcal{L}^{1}(\mu)$, and they are equal. Conversely, let $\mu$ be a measure on $(X,\mathcal{F})$ and $I$ the integral with respect to $\mu$. Then $\alpha$ holds and $I$ is a function. Every pair $(f,r)\in I$ has $f\in\mathcal{L}^{1}(\mu)$ and $r=I(f)=\int f\,d\mu$, so the third conjunct holds by $(*)$; and if $\varphi$ holds with $\mu$, $f$ and some set $r$, then $f\in\mathcal{L}^{1}(\mu)$ by $(*)$, so $(f,I(f))\in I$ and the last conjunct holds. So $\beta$ holds, and $\beta$ is a predicative formula in $x_{0},x_{1}$ expressing the condition of (ii) with $\mu=x_{0}$ and $I=x_{1}$. 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}$ expressing this condition with $\mu=x_{i}$ and $I=x_{j}$. This proves (ii).

The classes. Let $\mu$ be a measure on $(X,\mathcal{F})$. Then $(X,\mathcal{F},\mu)$ is a measure space (Measure, Measure Space, and Probability Measure (ii)), so the set $\mathcal{L}^{1}(\mu)$ of Integrable Functions and Their Lebesgue Integral (ii) and the integral with respect to $\mu$ of Integrable Functions and Their Lebesgue Integral (iii) are defined.

For (iii), let $C=\mathcal{L}^{1}(\mu)$, a set. For every class $a$, $a\in C$ if and only if $a\in\mathcal{L}^{1}(\mu)$. This proves (iii).

For (iv), let $\Lambda$ be the integral with respect to $\mu$, a map $\Lambda:\mathcal{L}^{1}(\mu)\to\mathbb{R}$. As $\mathcal{L}^{1}(\mu)$ and $\mathbb{R}$ are sets, $\Lambda$ is an element of the set of functions from $\mathcal{L}^{1}(\mu)$ to $\mathbb{R}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), hence a set. Let $D=\{\Lambda\}$ be its singleton, a set whose only element is $\Lambda$. For every class $a$, $a$ is the integral with respect to $\mu$ if and only if $a=\Lambda$, so $a\in D$ if and only if $a=\Lambda$. This proves (iv).