Proof 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

Proof of (i). For $c\in T$, the singleton $\{c\}$ is the defined set symbol given by the predicative formula $\forall w\,(w\in z\Leftrightarrow w=c)$ of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iv), and $u^{-1}(V)$ is the defined set symbol with argument $V$ and parameter $u$ given by the predicative formula $\pi(z,V)$ of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), used properly at every set $V$. By that clause, $u^{-1}(\{c\})$ is a subset of $S$, hence an element of $\mathcal{P}(S)$ by The Union Set and the Power Set of a Set (ii). So Maps and Relations Given by Formulas (i), with $T$ for $a$, $\mathcal{P}(S)$ for $b$ and $t(c)=u^{-1}(\{c\})$, gives exactly one map $\varphi:T\to\mathcal{P}(S)$ with $\varphi(c)=u^{-1}(\{c\})$ for every $c\in T$; by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v) it is the only set $h$ satisfying the predicative formula $\mu(h,T,\mathcal{P}(S))\wedge\forall c\,(c\in T\Rightarrow(c,u^{-1}(\{c\}))\in h)$, with $\mu$ as there.

Proof of (ii). Let $P=s[X]\times t[X]$, a subset of $\mathbb{R}\times\mathbb{R}$, finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (v). Let $x\in X$. As $(x,s(x))\in s$ and $(x,t(x))\in t$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), $s(x)\in s[X]$ and $t(x)\in t[X]$ by The Image and the Preimage of a Class under a Class (i), so $p=(s(x),t(x))\in P$; and $h(x)=F(p)$ with $(p,F(p))\in F$, so $h(x)\in F[P]$. Every element $b$ of $h[X]$ satisfies $(x,b)\in h$ for some $x\in X$, by The Image and the Preimage of a Class under a Class (i), so $b=h(x)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), and $b\in F[P]$. Thus $h[X]\subseteq F[P]$. The restriction $F|_{P}$ is a map $P\to\mathbb{R}$ with image $F[P]$, which is therefore finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi), and $h[X]$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv).

Proof of (iii). Let $\mathrm{ev}:[-\infty,\infty]^{X}\times X\to[-\infty,\infty]$ be the evaluation map of Projection, Evaluation and Currying Maps (ii), so that $f_{m}(x)=\mathrm{ev}(f_{m},x)$, and let $\le$ on $\mathbb{N}$ be the order of $\mathbb{N}_{0}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v). Let $\mathrm{Inf},\mathrm{Sup}:\mathcal{P}([-\infty,\infty])\to[-\infty,\infty]$ be the maps of Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (iv), with $\mathrm{Inf}(e)=\inf e$ and $\mathrm{Sup}(e)=\sup e$.

For $(k,x)\in\mathbb{N}\times X$ and $j\in\mathbb{N}_{0}$ we have $k+j\in\mathbb{N}$: $k+j\in\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv), and $k+j\neq0$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (viii), as $k\neq0$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), so $k+j\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii). Now take the guard $k\in\mathbb{N}\wedge x\in X\wedge j\in\mathbb{N}_{0}$, for the variables $k,x,j$, with the map $f:\mathbb{N}\to[-\infty,\infty]^{X}$ of Sequences (i), the map $\mathrm{ev}$ and the addition $\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv) as parameters. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), $k$ and $j$ are terms of type $\mathbb{N}_{0}$, as $\mathbb{N}\subseteq\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), and $x$ is a term of type $X$. The sum $k+j$, the value of the addition at $(k,j)$, is a term of type $\mathbb{N}_{0}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv) and Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), and its value lies in $\mathbb{N}$ by the argument just given, so it is a term of type $\mathbb{N}$, the condition in Terms and Typed Terms under a Guard (iv) not depending on the type. Hence $f(k+j)$ is a term of type $[-\infty,\infty]^{X}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), $(f(k+j),x)$ a term of type $[-\infty,\infty]^{X}\times X$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), and $\mathrm{ev}(f(k+j),x)$ a term of type $[-\infty,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), with value $f_{k+j}(x)$. Let

$$E(k,x)=\{\mathrm{ev}(f(k+j),x):j\in\mathbb{N}_{0}\}$$

be its image, as in Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (i) with $j$ as the variable ranging over the set $\mathbb{N}_{0}$. By that clause, $b\in E(k,x)$ if and only if $b=f_{k+j}(x)$ for some $j\in\mathbb{N}_{0}$; and for $m\in\mathbb{N}$, $k\le m$ if and only if $m=k+j$ for some $j\in\mathbb{N}_{0}$, by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (vii). So $E(k,x)=\{\mathrm{ev}(f(m),x):m\in D_{k}\}$ with $D_{k}=\{m\in\mathbb{N}:k\le m\}$, that is $E(k,x)=\{f_{m}(x):m\in\mathbb{N},\ m\ge k\}$, and $E(k,x)\in\mathcal{P}([-\infty,\infty])$ by Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (iv). By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (v), $E(k,x)$ is a defined set symbol with arguments $k$ and $x$, used properly where $k\in\mathbb{N}$ and $x\in X$, so it may stand as $t(v,w)$ in Maps and Relations Given by Formulas (ii) (that clause of Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term is stated for Maps and Relations Given by Formulas (i), and applies likewise to Maps and Relations Given by Formulas (ii) with two arguments), which gives a map $\Phi:\mathbb{N}\times X\to\mathcal{P}([-\infty,\infty])$ with $\Phi(k,x)=E(k,x)$. The composites $G=\mathrm{Inf}\circ\Phi$ and $H=\mathrm{Sup}\circ\Phi$ of Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii) are maps $\mathbb{N}\times X\to[-\infty,\infty]$ with $G(k,x)=\inf E(k,x)=\inf_{m\ge k}f_{m}(x)$ and $H(k,x)=\sup_{m\ge k}f_{m}(x)$, by Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (i).

By Projection, Evaluation and Currying Maps (iii) there is exactly one map $g:\mathbb{N}\to[-\infty,\infty]^{X}$ with $g(k)(x)=G(k,x)$ for all $k\in\mathbb{N}$ and $x\in X$. By Sequences (i) it is a sequence $(g_{k})$ in $[-\infty,\infty]^{X}$ with $g_{k}(x)=\inf_{m\ge k}f_{m}(x)$, and every such sequence is a map $\mathbb{N}\to[-\infty,\infty]^{X}$ with these values, hence equal to $g$ by the uniqueness in Projection, Evaluation and Currying Maps (iii). Applied to $H$, the same clause gives the only sequence $(h_{k})$ with $h_{k}(x)=\sup_{m\ge k}f_{m}(x)$.

Likewise, under the guard $x\in X\wedge k\in\mathbb{N}$, for the variables $x,k$, with $g$, $h$ and $\mathrm{ev}$ as parameters, $x$ and $k$ are terms of type $X$ and $\mathbb{N}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), so $g(k)$ and $h(k)$ are terms of type $[-\infty,\infty]^{X}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), $(g(k),x)$ and $(h(k),x)$ terms of type $[-\infty,\infty]^{X}\times X$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), and $\mathrm{ev}(g(k),x)$ and $\mathrm{ev}(h(k),x)$ terms of type $[-\infty,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), with values $g_{k}(x)$ and $h_{k}(x)$. For $x\in X$ let

$$D(x)=\{\mathrm{ev}(g(k),x):k\in\mathbb{N}\},\qquad D'(x)=\{\mathrm{ev}(h(k),x):k\in\mathbb{N}\}$$

be their images, as in Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (i) with $k$ as the variable ranging over the set $\mathbb{N}$; so $D(x)=\{g_{k}(x):k\in\mathbb{N}\}$ and $D'(x)=\{h_{k}(x):k\in\mathbb{N}\}$, and both lie in $\mathcal{P}([-\infty,\infty])$ by Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (iv). By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (v), with $x$ as the $u$ there and values in the set $\mathcal{P}([-\infty,\infty])$, they may stand as $t(u)$ in Maps and Relations Given by Formulas (i), which gives maps $\Psi,\Psi':X\to\mathcal{P}([-\infty,\infty])$ with $\Psi(x)=D(x)$ and $\Psi'(x)=D'(x)$, and $L=\mathrm{Sup}\circ\Psi$ and $U=\mathrm{Inf}\circ\Psi'$ are maps $X\to[-\infty,\infty]$ with $L(x)=\sup\{g_{k}(x):k\in\mathbb{N}\}$ and $U(x)=\inf\{h_{k}(x):k\in\mathbb{N}\}$. They are the only such maps, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). For $x\in X$, $g_{k}(x)=\inf_{m\ge k}f_{m}(x)$ and $h_{k}(x)=\sup_{m\ge k}f_{m}(x)$ for every $k\in\mathbb{N}$, so $L(x)=\liminf_{m\to\infty}f_{m}(x)$ by Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii) and $U(x)=\limsup_{m\to\infty}f_{m}(x)$ by Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (iii).

Proof of (iv). Let $j:\mathbb{Z}\to\mathbb{Q}$ be the map of The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist (iii), injective and preserving sums and the order by The Rational Numbers Form an Archimedean Ordered Field Containing the Integers (ii), and let $\kappa:\mathbb{Q}\to\mathbb{R}$ be the canonical embedding of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (iv) into $\mathbb{R}$, an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i). By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v), an integer $n$ read in $\mathbb{R}$ is the real number $\kappa(j(n))$, and by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi) the order and the sum of integers agree with those of $\mathbb{R}$ in this reading. Let $\theta(n,z)$ be the formula $n\in\mathbb{Z}\wedge\kappa(j(n))\le z\wedge z<\kappa(j(n))+1$, with the order, the strict order, the sum and the element $1$ of $\mathbb{R}$. It is written with values of maps and of a binary operation, defined set symbols used properly by the left conjunct $n\in\mathbb{Z}$, and with memberships in the order relation, and quantifies over sets only; so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). For $z\in\mathbb{R}$ exactly one set $n$ satisfies $\theta(n,z)$, by The Integers in the Real Numbers: Greatest Elements, the Integer Part, and Archimedean Consequences (iv) read in this way, and it is $\lfloor z\rfloor$ by The Integer Part of a Real Number (i).

So, for the variable $z$ and the guard $z\in\mathbb{R}$, with $j$ and $\kappa$ as parameters, $\lfloor z\rfloor$ is a term of type $\mathbb{Z}$ under $z\in\mathbb{R}$: its value lies in $\mathbb{Z}$, and for a set variable $w$ other than $z$, $j$ and $\kappa$, the condition $z\in\mathbb{R}\wedge w=\lfloor z\rfloor$ is expressed by the predicative formula $z\in\mathbb{R}\wedge\theta(w,z)$. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), applied first with the map $j$ and then with the map $\kappa$, $\kappa(j(\lfloor z\rfloor))$, which is $\lfloor z\rfloor$ read in $\mathbb{R}$, is a term of type $\mathbb{R}$ under $z\in\mathbb{R}$; so, by Terms and Typed Terms under a Guard (iv), the condition $z\in\mathbb{R}\wedge w=\kappa(j(\lfloor z\rfloor))$ is expressed by a predicative formula $\rho(w,z)$. For $z\in\mathbb{R}$ exactly one set $w$ satisfies $\rho(w,z)$, so $\lfloor z\rfloor$ read in $\mathbb{R}$ is a defined set symbol with argument $z$, given by $\rho$ and used properly where $z\in\mathbb{R}$, and it lies in $\mathbb{R}$. Hence Maps and Relations Given by Formulas (i), with $\mathbb{R}$ for $a$ and $b$, gives exactly one map $\lfloor\cdot\rfloor:\mathbb{R}\to\mathbb{R}$ with value $\lfloor z\rfloor$ at every $z\in\mathbb{R}$. For a set $X$ and a map $y:X\to\mathbb{R}$, the composite $\lfloor\cdot\rfloor\circ y$ is, by Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), the only map $X\to\mathbb{R}$ with value $\lfloor y(x)\rfloor$ at every $x\in X$.

Proof of (v). Let $\rho(p)$ be the formula $\exists a\,\exists x\,(p=(a,x)\wedge x\in a)$; it quantifies over sets only, the ordered pair being a defined set symbol by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (v), so it is predicative. For $A\in\mathcal{P}(X)$ and $x\in X$, $\rho((A,x))$ holds if and only if $x\in A$, by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i). By Maps Defined by Cases (i), with the set $\mathcal{P}(X)\times X$, the property $\rho$ and the expressions $1$ and $0$, elements of $\mathbb{R}$, there is a map $G:\mathcal{P}(X)\times X\to\mathbb{R}$ with $G(A,x)=1$ if $x\in A$ and $G(A,x)=0$ if $x\notin A$. By Projection, Evaluation and Currying Maps (iii) there is exactly one map $I:\mathcal{P}(X)\to\mathbb{R}^{X}$ with $I(A)(x)=G(A,x)$ for all $A\in\mathcal{P}(X)$ and $x\in X$. For $A\in\mathcal{P}(X)$, $A\subseteq X$ by The Union Set and the Power Set of a Set (ii), and $I(A)$ and $\mathbf{1}_{A}$ are maps $X\to\mathbb{R}$ with the same value at every $x\in X$, by Indicator Function of a Subset (i); so $I(A)=\mathbf{1}_{A}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). If $I':\mathcal{P}(X)\to\mathbb{R}^{X}$ also satisfies $I'(A)=\mathbf{1}_{A}$ for every $A\in\mathcal{P}(X)$, then $I'(A)(x)=\mathbf{1}_{A}(x)=G(A,x)$ for all $A$ and $x$, so $I'=I$ by the uniqueness in Projection, Evaluation and Currying Maps (iii).