Proof of Operations over the Finite Images of Maps, and the Summands of the Simple Integral

Proof of (i). Let $X$, $T$, $Y$, $\ast$, $e$, $A$ and $G$ be as there.

The summand maps. Let $s\in A$. For every $v\in s[X]$ there is $u\in X$ with $(u,v)\in s$, by The Image and the Preimage of a Class under a Class (i), so $v=s(u)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), and $v\in T$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii); thus $s[X]\subseteq T$, and $s[X]$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set (i). For $c\in T$, $(s,c)\in A\times T$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), so the value $G(s,c)=G((s,c))$ is used properly and lies in $Y$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). Hence Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), applied with $T$ for $A$ and $Y$ for $B$ there, $k=1$, the set variable $s$ for $v_{1}$, the guard $s\in A$ for $\gamma$ and the expression $G((s,c))$, built from variables and the defined set symbols for values and ordered pairs, for $t(c,s)$, gives a predicative formula $\theta(h,s)$ such that, for every $s\in A$, the only set $h$ satisfying $\theta(h,s)$ is the map $g_{s}:T\to Y$, $c\mapsto G(s,c)$. Its restriction $g_{s}|_{s[X]}$ is a map $s[X]\to Y$ with value $G(s,c)$ at every $c\in s[X]$, by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii), so it is the map $c\mapsto G(s,c)$ from $s[X]$ to $Y$ of the statement, which exists and is unique by Maps and Relations Given by Formulas (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv); this map is its own restriction to $s[X]$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii), so its operation over $s[X]$ in the sense of Sums and Products over a Finite Set and over an Interval (iii) is its operation over $s[X]$ as in Sums and Products over a Finite Set and over an Interval (i) and Sums and Products over a Finite Set and over an Interval (ii). As $s[X]$ is finite and $\ast$ has the neutral element $e$, $\mathop{\ast}\limits_{c\in s[X]}G(s,c)$ is defined, by Sums and Products over a Finite Set and over an Interval (i) and Sums and Products over a Finite Set and over an Interval (ii); it is also the operation over $s[X]$ of $g_{s}$ in the sense of Sums and Products over a Finite Set and over an Interval (iii), and it lies in $Y$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (ii).

A predicative formula for the value. Let $C$, $h$ and $w$ be set variables distinct from each other and from $s$. Let $\iota(C,s)$ be the formula $\forall v\,(v\in C\Leftrightarrow\exists u\,(u\in X\wedge(u,v)\in s))$; it quantifies over sets only, and $(u,v)\in s$ is 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), formed as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i), so it is predicative, and for $s\in A$ the only set $C$ satisfying it is $s[X]$, by The Image and the Preimage of a Class under a Class (i) and Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii), as $s[X]$ is a set. Let $\mathrm{fop}(w,C,h)$ be the predicative formula of Iterated Operations over Finite Sets Are Given by a Predicative Formula (i), formed for the set variables $w$, $C$, $h$ in place of $w$, $C$, $g$ there and for class variables $X_{1},\dots,X_{5}$ in place of $X$, $F$, $Y$, $R$ and $P$ there, which are assigned the set $Y$, the operation $\ast$, $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$, respectively (it stays predicative under this choice of variables 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 (i), its memberships of ordered pairs and of pairs of ordered pairs being read as in 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) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv)). Let

$$\psi(w,s)\ :\ \exists C\,\exists h\,\bigl(\iota(C,s)\wedge\theta(h,s)\wedge\mathrm{fop}(w,C,h)\bigr).$$

It 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). Let $s\in A$ and let $w$ be a set. As $s[X]$ and $g_{s}$ are the only sets satisfying $\iota(C,s)$ and $\theta(h,s)$, $\psi(w,s)$ holds if and only if $\mathrm{fop}(w,s[X],g_{s})$ holds. Here $s[X]$ is finite and $g_{s}$ is a map from the set $T$, which contains $s[X]$, to $Y$; so, by Iterated Operations over Finite Sets Are Given by a Predicative Formula (i), $\mathrm{fop}(w,s[X],g_{s})$ holds if and only if $w$ is the operation over $s[X]$ of $g_{s}$, that is, $w=\mathop{\ast}\limits_{c\in s[X]}G(s,c)$, by the first part.

The map. Thus, for every $s\in A$, exactly one set $w$ satisfies $\psi(w,s)$, namely $\mathop{\ast}\limits_{c\in s[X]}G(s,c)$; so this is a defined set symbol with argument $s$, given by the predicative formula $\psi$ and used properly where $s\in A$. It lies in $Y$ for every $s\in A$, by the first part. Hence Maps and Relations Given by Formulas (i), with $A$ for $a$, $Y$ for $b$ and $t(s)=\mathop{\ast}\limits_{c\in s[X]}G(s,c)$, gives exactly one map $I:A\to Y$ with $I(s)=\mathop{\ast}\limits_{c\in s[X]}G(s,c)$ for every $s\in A$, which proves (i).

Proof of (ii). Let $(X,\mathcal{F})$, $\mu$ and $A$ be as there. Let $s\in A$ and $c\in[0,\infty]$. The singleton $\{c\}$ is a subset of $[0,\infty]$, and $s^{-1}(\{c\})\in\mathcal{F}$ by hypothesis; as $\mu$ is a map from $\mathcal{F}$ to $[0,\infty]$, by Measure, Measure Space, and Probability Measure (i), $\mu(s^{-1}(\{c\}))\in[0,\infty]$, and so $c\cdot\mu(s^{-1}(\{c\}))\in[0,\infty]$, as $\cdot$ is a binary operation on $[0,\infty]$ by Addition and Multiplication on [0,∞] (ii).

Let $f$ be a set variable other than the variables $z$, $V$, $s$ and $w$ of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), and let $t(f,c)$ be the expression $c\cdot\mu(f^{-1}(\{c\}))$. It is built from variables and defined set symbols: the singleton $\{c\}$ is a defined set symbol with argument $c$, given by the predicative formula of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iv) and used properly at every set $c$; for every $f\in A$, $f^{-1}(V)$ is a defined set symbol with argument $V$ and parameter $f$, given by the predicative formula $\pi$ of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), applied with $X$ for $S$, $[0,\infty]$ for $T$ and the variable $f$, whose value is the map $f$, for $u$, and used properly at every set $V$; the value $\mu(z)$ of $\mu$ at a set $z\in\mathcal{F}$ is the only set $y$ with $(z,y)\in\mu$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), a predicative formula 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); and the product $x\cdot y$ of $x,y\in[0,\infty]$ is the only set $z$ with $((x,y),z)\in\cdot$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), a predicative formula 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 (iv). By the first paragraph, for $f\in A$ and $c\in[0,\infty]$ each of these symbols is used properly where it occurs in $t(f,c)$, and $t(f,c)\in[0,\infty]$. Hence Maps and Relations Given by Formulas (ii), applied with $[0,\infty]$ for $b$ and $d$, $A$ for its $c$ and $t(f,c)$ for $t(v,w)$, gives exactly one map $G:A\times[0,\infty]\to[0,\infty]$ with $G(s,c)=G((s,c))=c\cdot\mu(s^{-1}(\{c\}))$ for all $s\in A$ and $c\in[0,\infty]$, which proves (ii).