The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Measurable Functions and the Lebesgue Integral: Notation, let $(X,\mathcal{F})$ be a measurable space; this item is a statement of the metatheory. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k<N$, not necessarily distinct. Each clause states that a condition on $x_{0},\dots,x_{N-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. The other letters, among them $X$, $\mathcal{F}$, the sets of numbers with their operations and orders, and the class $M$ of (iv), are parameters.

For a map $m:\mathcal{F}\to[0,\infty]$, not necessarily a measure, $I_{m}(s)$, $\int g\,dm$, $\mathcal{L}^{1}(m)$ and $\int f\,dm$ are formed, with $m$ in place of the measure, by the formulas of Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv), Nonnegative Measurable Maps and Their Lebesgue Integral (ii), Integrable Functions and Their Lebesgue Integral (ii) and Integrable Functions and Their Lebesgue Integral (iii).

(i) The simple integral. With $m=x_{i}$, $s=x_{j}$ and $r=x_{k}$: "$m$ is a map $m:\mathcal{F}\to[0,\infty]$, $s\in\mathcal{S}^{+}$ and $r=I_{m}(s)$".

(ii) The integral of a nonnegative function. With $m=x_{i}$, $g=x_{j}$ and $r=x_{k}$: "$m$ is a map $m:\mathcal{F}\to[0,\infty]$, $g\in\mathcal{M}^{+}$ and $r=\int g\,dm$".

(iii) The integral of an integrable function. With $m=x_{i}$, $f=x_{j}$ and $r=x_{k}$: "$m$ is a map $m:\mathcal{F}\to[0,\infty]$, $f\in\mathcal{L}^{1}(m)$ and $r=\int f\,dm$".

(iv) The integral against a finite signed measure. Assume the axiom of dependent choice, and let $M$ be a class of finite signed measures on $(X,\mathcal{F})$; for $\nu\in M$, $\mathcal{L}^{1}(\nu)$ and $\int f\,d\nu$ are as in Integrable Functions and the Integral with Respect to a Finite Signed Measure (i) and Integrable Functions and the Integral with Respect to a Finite Signed Measure (ii). With $\nu=x_{i}$, $f=x_{j}$ and $r=x_{k}$: "$\nu\in M$, $f\in\mathcal{L}^{1}(\nu)$ and $r=\int f\,d\nu$".