Proof of Monotone Convergence Theorem

Throughout, $\le$ on $[-\infty,\infty]$ is a total order agreeing with the order of $\mathbb{R}$ on $\mathbb{R}$ (Order and Suprema in the Extended Real Line (i)), and $<$ is its strict relation; for $u,v,w\in[-\infty,\infty]$ with $u<v$ and $v\le w$ we have $u<w$, by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (v) and Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iv). Let $\mathcal{S}^{+}=\mathcal{S}^{+}(X,\mathcal{F})$ and $I_{\mu}$ be the set of nonnegative simple functions and the simple integral of Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iii) and Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv), and for $g\in\mathcal{M}^{+}$ let $\Sigma_{g}=\{I_{\mu}(t):t\in\mathcal{S}^{+},\ t(x)\le g(x)\text{ for every }x\in X\}$, so that $\int_{X}g\,d\mu=\sup\Sigma_{g}$ by Nonnegative Measurable Maps and Their Lebesgue Integral (ii). By Nonnegative Measurable Maps and Their Lebesgue Integral (i), $(f_{m})$ is a sequence in $[0,\infty]^{X}$. For $x\in X$ let $u^{x}$ be the sequence in $[0,\infty]$ with $u^{x}_{m}=f_{m}(x)$ for every $m\in\mathbb{N}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (i)); its range $\operatorname{ran}u^{x}$ is $\{f_{m}(x):m\in\mathbb{N}\}$ by Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (ii), so by hypothesis $f(x)=\sup\operatorname{ran}u^{x}$.

Proof of (i). By Nonnegative Measurable Maps and Their Lebesgue Integral (i), $(f_{m})$ is a sequence in $\mathrm{Meas}(X,\mathcal{F};[0,\infty],\mathcal{B}([0,\infty]))$. By Suprema, Infima, Limits Inferior and Limits Superior of Measurable [0,∞]-Valued Maps (i), with $J=\mathbb{N}$, the map $x\mapsto\sup_{m}f_{m}(x)$ from $X$ to $[0,\infty]$ is measurable; it is $f$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv), as both have the value $\sup\{f_{m}(x):m\in\mathbb{N}\}$ at every $x\in X$: $f(x)=\sup\operatorname{ran}u^{x}$ and $\operatorname{ran}u^{x}=\{f_{m}(x):m\in\mathbb{N}\}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (ii)). So $f\in\mathcal{M}^{+}$ by Nonnegative Measurable Maps and Their Lebesgue Integral (i).

Proof of (ii): the inequality $\le$. Let $v:\mathbb{N}\to[0,\infty]$ be the composite (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)) of the sequence $(f_{m})$ with the integral map $\mathcal{M}^{+}\to[0,\infty]$ of Nonnegative Measurable Maps and Their Lebesgue Integral (ii), the sequence with $v_{m}=\int_{X}f_{m}\,d\mu$; its range is $\operatorname{ran}v=v[\mathbb{N}]=\{v_{m}:m\in\mathbb{N}\}$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (v), The Image and the Preimage of a Class under a Class (i)), so $\alpha=\sup_{m}\int_{X}f_{m}\,d\mu$ is $\sup\operatorname{ran}v$. As $\operatorname{ran}v\subseteq[0,\infty]$ is nonempty ($v_{1}\in\operatorname{ran}v$, as $1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (ii)), $\alpha$ exists and lies in $[0,\infty]$ by Order and Suprema in the Extended Real Line (iii) and Order and Suprema in the Extended Real Line (ix). For $m\in\mathbb{N}$ and $x\in X$, $f_{m}(x)\le f(x)$, since $f_{m}(x)=u^{x}_{m}\in\operatorname{ran}u^{x}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (ii)) and $f(x)=\sup\operatorname{ran}u^{x}$ is an upper bound of $\operatorname{ran}u^{x}$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)); so $\int_{X}f_{m}\,d\mu\le\int_{X}f\,d\mu$ by Basic Properties of the Integral of Nonnegative Measurable Maps (iii), which applies as $f\in\mathcal{M}^{+}$ by (i). Thus $\int_{X}f\,d\mu$ is an upper bound of $\operatorname{ran}v$, whose elements are the integrals $v_{m}=\int_{X}f_{m}\,d\mu$, and $\alpha\le\int_{X}f\,d\mu$ because $\alpha$ is their least upper bound (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)).

The inequality $\ge$. Since $\int_{X}f\,d\mu=\sup\Sigma_{f}$ is the least upper bound of $\Sigma_{f}$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)), it suffices to show that $I_{\mu}(s)\le\alpha$ for every $s\in\mathcal{S}^{+}$ with $s(x)\le f(x)$ for every $x\in X$. Fix such an $s$; then fix a real number $c$ with $0<c<1$; the index $m$ is chosen last.

The sets $E_{m}$. As $s\in\mathcal{S}^{+}\subseteq\mathcal{S}$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iii)), the scalar multiple $cs$ lies in $\mathcal{S}$ by Properties of Simple Functions and of the Simple Integral (ii), with $(cs)(x)=c\,s(x)$ for $x\in X$ (Pointwise Operations on Real-Valued Maps (i)). By The Strict Level Sets of a Sequence of Nonnegative Measurable Maps above a Simple Function Form a Sequence of Measurable Sets (i), applied to $cs$ and $(f_{m})$, there is a sequence $(E_{m})$ in $\mathcal{F}$ with $E_{m}=\{x\in X:c\,s(x)<f_{m}(x)\}$ for every $m\in\mathbb{N}$. Further, $E_{m}\subseteq E_{m+1}$: if $c\,s(x)<f_{m}(x)$, then $c\,s(x)<f_{m+1}(x)$ as $f_{m}(x)\le f_{m+1}(x)$. Let $A=\bigcup_{m\in\mathbb{N}}E_{m}$, which lies in $\mathcal{F}$ by σ-Algebra and Measurable Space (i). Let $x\in X$ with $s(x)\neq0$. Then $s(x)$ is real with $0<s(x)$, and $0<1-c$, so $0<(1-c)\,s(x)=s(x)-c\,s(x)$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (iv), that is $c\,s(x)<s(x)$; hence $c\,s(x)<s(x)\le f(x)=\sup\operatorname{ran}u^{x}$, by the transitivity noted above, and Order and Suprema in the Extended Real Line (x) gives an element of $\operatorname{ran}u^{x}$ above $c\,s(x)$, which is $f_{m}(x)$ for some $m\in\mathbb{N}$ by Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (ii); so $x\in E_{m}\subseteq A$. Therefore $s\mathbf{1}_{A}=s$: for $x\in A$, $(s\mathbf{1}_{A})(x)=s(x)\cdot1=s(x)$, and for $x\in X$ with $x\notin A$, $s(x)=0$ and $(s\mathbf{1}_{A})(x)=s(x)\cdot0=0=s(x)$, by Pointwise Operations on Real-Valued Maps (i), Indicator Function of a Subset (i), Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (v) and Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (vii); so $s\mathbf{1}_{A}=s$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

The measure $\nu$. Let $\iota:\mathcal{P}(X)\to\mathbb{R}^{X}$, $B\mapsto\mathbf{1}_{B}$, be the map of Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators (v). Currying the pointwise product $\mathbb{R}^{X}\times\mathbb{R}^{X}\to\mathbb{R}^{X}$ of Pointwise Operations on Real-Valued Maps (i) by Projection, Evaluation and Currying Maps (iii) gives a map $h:\mathbb{R}^{X}\to(\mathbb{R}^{X})^{\mathbb{R}^{X}}$ with $h(g)(g')=gg'$, and $P_{s}=h(s):\mathbb{R}^{X}\to\mathbb{R}^{X}$, $g\mapsto sg$. The composite $P_{s}\circ\iota:\mathcal{P}(X)\to\mathbb{R}^{X}$ has the value $s\mathbf{1}_{B}$ at $B$, and its restriction to $\mathcal{F}\subseteq\mathcal{P}(X)$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix)) has its values in $\mathcal{S}^{+}$ by Properties of Simple Functions and of the Simple Integral (i) and Properties of Simple Functions and of the Simple Integral (ii), so it is a map $\mathcal{F}\to\mathcal{S}^{+}$. Let $\nu:\mathcal{F}\to[0,\infty]$ be its composite with $I_{\mu}$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv)), so that $\nu(B)=I_{\mu}(s\mathbf{1}_{B})$ for every $B\in\mathcal{F}$; it is a measure on $(X,\mathcal{F})$ by Properties of Simple Functions and of the Simple Integral (vii), so $(X,\mathcal{F},\nu)$ is a measure space (Measure, Measure Space, and Probability Measure (ii)). Let $w=\nu\circ E:\mathbb{N}\to[0,\infty]$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)), the sequence with $w_{m}=\nu(E_{m})$, whose range is $\operatorname{ran}w=\{w_{m}:m\in\mathbb{N}\}$ as for $v$. By Basic Properties of a Measure (viii), applied to $\nu$ and $(E_{m})$, and as $s\mathbf{1}_{A}=s$, $I_{\mu}(s)=\nu(A)=\sup\operatorname{ran}w$.

Comparison with $\int_{X}f_{m}\,d\mu$. Let $m\in\mathbb{N}$ and $\varphi_{m}=c\,(s\mathbf{1}_{E_{m}})$. By Properties of Simple Functions and of the Simple Integral (i) and Properties of Simple Functions and of the Simple Integral (ii), $s\mathbf{1}_{E_{m}}$ and $\varphi_{m}$ belong to $\mathcal{S}^{+}$, and $I_{\mu}(\varphi_{m})=c\cdot I_{\mu}(s\mathbf{1}_{E_{m}})=c\cdot\nu(E_{m})=c\cdot w_{m}$ by Properties of Simple Functions and of the Simple Integral (v). For $x\in X$, $\varphi_{m}(x)=c\,(s(x)\,\mathbf{1}_{E_{m}}(x))$ (Pointwise Operations on Real-Valued Maps (i)), which is $c\,s(x)$ if $x\in E_{m}$ and $0$ otherwise, by Indicator Function of a Subset (i), Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (v) and Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (vii); so $\varphi_{m}(x)\le f_{m}(x)$ by the definition of $E_{m}$ and as $0\le f_{m}(x)$ (Order and Suprema in the Extended Real Line (viii)). So $I_{\mu}(\varphi_{m})\in\Sigma_{f_{m}}$, and $c\cdot w_{m}=I_{\mu}(\varphi_{m})\le\int_{X}f_{m}\,d\mu=v_{m}\le\alpha$, as $\int_{X}f_{m}\,d\mu=\sup\Sigma_{f_{m}}$ is an upper bound of $\Sigma_{f_{m}}$ and $v_{m}\in\operatorname{ran}v$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)).

Scaling the supremum. As $c\ge0$, $c\in[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii). Currying the product of $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)) by Projection, Evaluation and Currying Maps (iii) gives a map $M_{c}:[0,\infty]\to[0,\infty]$ with $M_{c}(u)=c\cdot u$, and $M_{c}\circ w$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)) has the value $c\cdot w_{m}$ at $m\in\mathbb{N}$; so its range $\operatorname{ran}(M_{c}\circ w)$ is $\{c\cdot u:u\in\operatorname{ran}w\}$, and $\alpha$ is an upper bound of it by the previous paragraph. By Suprema and Finite Sums in [0,∞] (ii), applied to the subset $\operatorname{ran}w$ of $[0,\infty]$, nonempty as $w_{1}\in\operatorname{ran}w$, and to $c$,

$$c\cdot I_{\mu}(s)=c\cdot\sup\operatorname{ran}w=\sup\{c\cdot u:u\in\operatorname{ran}w\}\le\alpha.$$

Letting $c$ increase to $1$. Thus $c\cdot I_{\mu}(s)\le\alpha$ for every real $c$ with $0<c<1$, such $c$ lying in $[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii), where $I_{\mu}(s)\in[0,\infty]$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv)) and $\alpha\in[0,\infty]$; so $I_{\mu}(s)\le\alpha$ by Greatest Elements as Suprema, Suprema and Infima of Nested Sets in [−∞,∞], and a Scaling Criterion for Order in [0,∞] (iii).

So $I_{\mu}(s)\le\alpha$ for every $s\in\mathcal{S}^{+}$ with $s(x)\le f(x)$ for every $x$, that is, $\alpha$ is an upper bound of $\Sigma_{f}$, and $\int_{X}f\,d\mu\le\alpha$. With the first inequality, $\int_{X}f\,d\mu=\alpha=\sup_{m}\int_{X}f_{m}\,d\mu$, by antisymmetry of $\le$ (Order and Suprema in the Extended Real Line (i)).