Proof of Kit for def:independence-events-rvs

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. Routine facts about sets, maps, natural numbers and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iv), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v)), and so is the agreement with the current versions of the earlier versions of the definitions of $\sigma$-algebras, measures, Borel $\sigma$-algebras, metric spaces, probability spaces, events, random elements and iterated operations that some cited items use (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 (ii), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence Agree (i), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (vi)). The formulas below are built in distinct set variables named after the objects they will carry, $\Omega$, $\mathcal{F}$, $P$, $J$, $\mathcal{C}$, $A$, $S$, $d$, $X$, $T$, $e$, $Y$, $\mathcal{G}$, $V$, $V'$, $K$, $S'$, $d'$, and in the bound set variables written below; these named and bound variables are pairwise distinct and different from $x_{0},\dots,x_{N-1}$ and from the eighteen parameters, which are at their fixed values (Conditions Expressed by a Predicative Formula, and Guards (i)); a formula taken from another item is used at the variables named, its bound variables chosen other than all of these and its parameters being the parameters of the statement with the same values. The formula given below for each condition of the statement has its free variables among the parameters and the variables named in that condition, and is shown to express the condition at them; the last paragraph moves it to the positions given in the statement.

Formulas used. By Kit for def:probability-space-random-variable (i), with its $N$ equal to $3$, its variables $x_{0},x_{1},x_{2}$ being $\Omega,\mathcal{F},P$, its indices $i,j,k$ equal to $0,1,2$ and its seventeen parameters being those of the statement with the same names, which have the values and kinds that kit prescribes, there is a predicative formula $\mathrm{ps}(\Omega,\mathcal{F},P)$ expressing "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$ and $(\Omega,\mathcal{F},P)$ is a probability space". In the same way Kit for def:probability-space-random-variable (iv), with its $N$ equal to $6$, its variables $\Omega,\mathcal{F},P,S,d,X$ and its indices $0,\dots,5$, gives a predicative formula $\mathrm{re}(\Omega,\mathcal{F},P,S,d,X)$ expressing "$\mathrm{ps}(\Omega,\mathcal{F},P)$, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space and $X$ is a random element of $S$"; and Kit for def:random-element-law-metric (i), with its $N$ equal to $7$, its $x_{0},\dots,x_{6}$ being $\Omega,\mathcal{F},P,S,d,V,V'$ and its indices $i,j,k,l,m,p,q,r,s,t$ equal to $0,1,2,0,1,2,3,4,5,6$, so that its variables $\Omega,\mathcal{F},P,\Omega',\mathcal{F}',P',S,d,X,Y$ are here $\Omega,\mathcal{F},P,\Omega,\mathcal{F},P,S,d,V,V'$ (its $\Omega'$, $\mathcal{F}'$ and $P'$ are $\Omega$, $\mathcal{F}$ and $P$, and its $X$ and $Y$ are written $V$ and $V'$), gives a predicative formula $\mathrm{id}(\Omega,\mathcal{F},P,S,d,V,V')$ expressing "$\mathrm{ps}(\Omega,\mathcal{F},P)$, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, $V$ and $V'$ are random elements of $S$, and $V$ and $V'$ are identically distributed". Further, the parameters $R$ and $Q$ of the statement have as values the order and the addition of $\mathbb{N}_{0}$ (Sums of Sequences in [0,∞] as Typed Terms and as a Map (i)), and $\mathbb{N}$ the set of natural numbers, which is the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii); these are the values the two lemmas and the helper cited next give their parameters $R$, $Q$ (or $P$) and $\mathbb{N}$ (or $Y$), the helper's $\mathbb{R}$, $\le$, $<$, $+$ and $0$ being our $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$ and $0_{\mathbb{R}}$, and $\cdot_{\mathbb{R}}$ is a binary operation on $\mathbb{R}$ (The Real Numbers (iii)). So: by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), there is a predicative formula $\mathrm{seg}(z,n)$ such that, for every set $z$ and every $n\in\mathbb{N}_{0}$, $\mathrm{seg}(z,n)$ holds if and only if $z=[n]$; by Iterated Operations Are Given by a Predicative Formula (i), with the class variables $\mathbb{R}$, $\cdot_{\mathbb{R}}$, $\mathbb{N}$, $R$ and $Q$ as its $X$, $F$, $Y$, $R$ and $P$, there is a predicative formula $\mathrm{it}(c,n,b)$ such that, for every $n\in\mathbb{N}$, every map $b:[n]\to\mathbb{R}$ and every set $c$, $\mathrm{it}(c,n,b)$ holds if and only if $c=\prod_{h=1}^{n}b_{h}$, the finite product; by Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (iv) and Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (v), there are predicative formulas $\mathrm{sa}(\mathcal{H},\Omega)$ and $\mathrm{bo}(B,S,d)$ expressing "$\mathcal{H}$ is a $\sigma$-algebra on $\Omega$" and "$(S,d)$ is a metric space and $B\in\mathcal{B}(S,d)$", the Borel $\sigma$-algebra; and the formulas $\Phi(F)$, $\mu(F,A,B)$ and $\iota(F)$ 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), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) 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 (viii) are predicative and say that $F$ is a function, that $F$ is a map $F:A\to B$, and, for a map, that it is injective, at variables of either kind; formulas $(t_{1},t_{2})\in s$ and $((t_{1},t_{2}),t_{3})\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) 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). For variables $\mathcal{C}$ and $K$ let

$$\mathrm{fam}(\mathcal{C},K)=\Phi(\mathcal{C})\wedge\forall u\,\bigl(u\in K\Leftrightarrow\exists v\,((u,v)\in\mathcal{C})\bigr);$$

it is predicative, and for sets it holds if and only if $\mathcal{C}$ is a function with domain $K$, that is, a family $(\mathcal{C}_{t})_{t\in K}$ indexed by $K$; then, for $t\in K$ and a set $y$, $(t,y)\in\mathcal{C}$ if and only if $y=\mathcal{C}_{t}$.

Step 1: independent classes of events. Let $\alpha$ be the conjunction of the formulas

$$\begin{gathered} n\in\mathbb{N},\quad \mathrm{seg}(z,n),\quad \mu(f,z,J),\quad \iota(f),\quad \mu(a,z,\mathcal{F}),\quad \forall h\,\forall t\,\forall D\,\forall y\,\bigl(((h,t)\in f\wedge(t,D)\in\mathcal{C}\wedge(h,y)\in a)\Rightarrow y\in D\bigr),\\ \mu(b,z,\mathbb{R}),\quad \forall h\,\forall y\,\forall r\,\bigl(((h,y)\in a\wedge(h,r)\in b)\Rightarrow(y,r)\in P\bigr),\quad \forall u\,\bigl(u\in w\Leftrightarrow\forall h\,\forall y\,((h,y)\in a\Rightarrow u\in y)\bigr),\quad \mathrm{it}(c,n,b), \end{gathered}$$

and let

$$\mathrm{ind}(\mathcal{F},P,J,\mathcal{C})=\forall n\,\forall z\,\forall f\,\forall a\,\forall b\,\forall w\,\forall c\,\bigl(\alpha\Rightarrow(w,c)\in P\bigr).$$

All its quantifiers are over set variables, so it is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). Let sets $\Omega,\mathcal{F},P,J,\mathcal{C}$ be assigned such that $\mathrm{ps}(\Omega,\mathcal{F},P)$ holds and $\mathcal{C}=(\mathcal{C}_{t})_{t\in J}$ is a family of subsets of $\mathcal{F}$. We show that $\mathrm{ind}(\mathcal{F},P,J,\mathcal{C})$ holds if and only if $(\mathcal{C}_{t})_{t\in J}$ is independent in the sense of Independence of Classes of Events and of σ-Algebras (i). In that definition, distinct indices $j_{1},\dots,j_{n}\in J$ are an injective map $f:[n]\to J$, $h\mapsto j_{h}$, and events $A_{1}\in\mathcal{C}_{j_{1}},\dots,A_{n}\in\mathcal{C}_{j_{n}}$ are a family $(A_{h})_{h\in[n]}$, that is, a map $a:[n]\to\mathcal{F}$ with $a(h)\in\mathcal{C}_{f(h)}$ for every $h\in[n]$; $\bigcap_{h=1}^{n}A_{h}$ is the intersection of this family, an event (Probability Spaces: Notation (iii)); and $\prod_{h=1}^{n}P(A_{h})$ is the finite product of the map $h\mapsto P(a(h))$ from $[n]$ to $\mathbb{R}$ (Iterated Operations: Finite Sums and Finite Products (i)), the probability of an event being real (Events of a Probability Space: Subsets of Ω, Real Probabilities, Complements and Tail Unions (ii)).

First let sets $n,z,f,a,b,w,c$ satisfy $\alpha$. Then $n\in\mathbb{N}\subseteq\mathbb{N}_{0}$, so $z=[n]$; $f:[n]\to J$ is an injective map and $a:[n]\to\mathcal{F}$ a map. For $h\in[n]$, the sets $t=f(h)\in J$, $D=\mathcal{C}_{t}$ and $y=a(h)$ satisfy $(h,t)\in f$, $(t,D)\in\mathcal{C}$ and $(h,y)\in a$, so the sixth conjunct gives $a(h)\in\mathcal{C}_{f(h)}$. The map $b:[n]\to\mathbb{R}$ satisfies $(a(h),b(h))\in P$, that is, $b(h)=P(a(h))$, for every $h\in[n]$, as $P$ is a function. As $(h,y)\in a$ holds exactly when $h\in[n]$ and $y=a(h)$, the ninth conjunct says that $w$ has the elements of $\bigcap_{h\in[n]}a(h)$, so $w$ is this intersection. Finally $c=\prod_{h=1}^{n}b_{h}=\prod_{h=1}^{n}P(a(h))$.

If $(\mathcal{C}_{t})_{t\in J}$ is independent, then, for such sets, the definition applied to $n$, $f$ and $a$ gives $P(w)=c$; as $w$ is an event and $P$ a map on $\mathcal{F}$, $(w,c)\in P$. So $\mathrm{ind}$ holds.

Conversely let $\mathrm{ind}$ hold, and let $n\in\mathbb{N}$, an injective map $f:[n]\to J$ and a map $a:[n]\to\mathcal{F}$ with $a(h)\in\mathcal{C}_{f(h)}$ for every $h\in[n]$ be given. Let $z=[n]$, a set. Let $\psi(h,r)$ be the predicative formula $\exists y\,((h,y)\in a\wedge(y,r)\in P)$, with parameters $a$ and $P$ at the sets assigned; for every $h\in[n]$ exactly one $r\in\mathbb{R}$ satisfies it, namely $P(a(h))$, which is real (Events of a Probability Space: Subsets of Ω, Real Probabilities, Complements and Tail Unions (ii)). So there is a map $b:[n]\to\mathbb{R}$ with $b(h)=P(a(h))$ for every $h\in[n]$ (Maps from Functional Predicative Relations, and Families of Sections (ii)). Let $w=\bigcap_{h\in[n]}a(h)$, an event and so a set, and $c=\prod_{h=1}^{n}b_{h}$, a set as the value of a map into $\mathbb{R}$ (Iterated Operations: Finite Sums and Finite Products (i)). Then $n,z,f,a,b,w,c$ satisfy $\alpha$: for the sixth conjunct, $(h,t)\in f$, $(t,D)\in\mathcal{C}$ and $(h,y)\in a$ give $t=f(h)$, $D=\mathcal{C}_{t}$ and $y=a(h)\in\mathcal{C}_{f(h)}=D$; the others hold by the choice of $z$, $b$, $w$ and $c$ and the description of their elements and values. Hence $(w,c)\in P$, that is,

$$P\Bigl(\bigcap_{h=1}^{n}a(h)\Bigr)=\prod_{h=1}^{n}P\bigl(a(h)\bigr).$$

As $n$, $f$ and $a$ were arbitrary, $(\mathcal{C}_{t})_{t\in J}$ is independent.

Step 2: the $\sigma$-algebra $\sigma(X)$. Let

$$\mathrm{sg}(U,\Omega,S,d,X)=\forall u\,(u\in U\Rightarrow u\in\Omega)\wedge\forall\mathcal{H}\,\Bigl(\bigl(\mathrm{sa}(\mathcal{H},\Omega)\wedge\forall B\,\bigl(\mathrm{bo}(B,S,d)\Rightarrow\exists y\,(\forall u\,(u\in y\Leftrightarrow\exists v\,(v\in B\wedge(u,v)\in X))\wedge y\in\mathcal{H})\bigr)\bigr)\Rightarrow U\in\mathcal{H}\Bigr)$$

and

$$\mathrm{sig}(D,\Omega,S,d,X)=\forall U\,\bigl(U\in D\Leftrightarrow\mathrm{sg}(U,\Omega,S,d,X)\bigr),$$

predicative formulas, as their quantifiers are over set variables. Let sets $\Omega,\mathcal{F},P,S,d,X$ be assigned such that $\mathrm{re}(\Omega,\mathcal{F},P,S,d,X)$ holds. Then $\sigma(X)=\sigma(\mathcal{C}_{X})$, with $\mathcal{C}_{X}=\{X^{-1}(B):B\in\mathcal{B}(S)\}$, is defined and is a $\sigma$-algebra on $\Omega$ contained in $\mathcal{F}$ (σ-Algebras Generated by Random Elements (i)). We show that, for every set $U$, $\mathrm{sg}(U,\Omega,S,d,X)$ holds if and only if $U\in\sigma(X)$. By The σ-Algebra Generated by a Set of Subsets (ii), $U\in\sigma(\mathcal{C}_{X})$ if and only if $U\subseteq\Omega$ and $U\in\mathcal{H}$ for every $\sigma$-algebra $\mathcal{H}$ on $\Omega$ with $\mathcal{C}_{X}\subseteq\mathcal{H}$. Every such $\mathcal{H}$ is a subset of the power set of $\Omega$ (σ-Algebra and Measurable Space (i)) and so a set, and for a set $\mathcal{H}$, $\mathrm{sa}(\mathcal{H},\Omega)$ holds exactly when $\mathcal{H}$ is a $\sigma$-algebra on $\Omega$. For every set $B$, $\mathrm{bo}(B,S,d)$ holds exactly when $B\in\mathcal{B}(S)$; and for such $B$, the formula $\forall u\,(u\in y\Leftrightarrow\exists v\,(v\in B\wedge(u,v)\in X))$ holds exactly when $y=X^{-1}(B)$, a set (Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), with the map $X:\Omega\to S$ as $u$ there). So the antecedent inside $\forall\mathcal{H}$ says that $\mathcal{H}$ is a $\sigma$-algebra on $\Omega$ with $X^{-1}(B)\in\mathcal{H}$ for every $B\in\mathcal{B}(S)$, that is, with $\mathcal{C}_{X}\subseteq\mathcal{H}$, and $\mathrm{sg}(U,\Omega,S,d,X)$ is the membership condition above. Consequently, for every set $D$, $\mathrm{sig}(D,\Omega,S,d,X)$ holds if and only if $D$ and the set $\sigma(X)$ have the same elements, that is, $D=\sigma(X)$.

Step 3: the product rule for two events. For predicative formulas $\beta(U)$ and $\beta'(U')$ let

$$\chi[\beta,\beta']=\forall U\,\forall U'\,\forall w\,\forall r\,\forall r'\,\forall c\,\Bigl(\bigl(\beta(U)\wedge\beta'(U')\wedge\forall u\,(u\in w\Leftrightarrow(u\in U\wedge u\in U'))\wedge(U,r)\in P\wedge(U',r')\in P\wedge((r,r'),c)\in\cdot_{\mathbb{R}}\bigr)\Rightarrow(w,c)\in P\Bigr),$$

a predicative formula. Let sets be assigned such that $\mathrm{ps}(\Omega,\mathcal{F},P)$ holds and every set satisfying $\beta$ or $\beta'$ is an element of $\mathcal{F}$. We show that $\chi[\beta,\beta']$ holds if and only if $P(U\cap U')=P(U)\,P(U')$ for all sets $U$ and $U'$ with $\beta(U)$ and $\beta'(U')$. Fix such $U$ and $U'$; for other $U,U'$ the implication holds trivially. They are events, so $U\cap U'\in\mathcal{F}$ (Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix)), the only set $w$ with the elements of $U\cap U'$ is $U\cap U'$, the only sets $r,r'$ with $(U,r),(U',r')\in P$ are $P(U),P(U')\in\mathbb{R}$ (Events of a Probability Space: Subsets of Ω, Real Probabilities, Complements and Tail Unions (ii)), and, $\cdot_{\mathbb{R}}$ being a map from $\mathbb{R}\times\mathbb{R}$ to $\mathbb{R}$, the only set $c$ with $((P(U),P(U')),c)\in\cdot_{\mathbb{R}}$ is $P(U)\,P(U')$. So the part of $\chi[\beta,\beta']$ after $\forall U\,\forall U'$ says, for these $U$ and $U'$, that $(U\cap U',P(U)\,P(U'))\in P$, that is, $P(U\cap U')=P(U)\,P(U')$.

Independent events. Let

$$\varepsilon=\mathrm{ps}(\Omega,\mathcal{F},P)\wedge\mathrm{fam}(A,J)\wedge\forall t\,\forall y\,((t,y)\in A\Rightarrow y\in\mathcal{F})\wedge\exists\mathcal{C}\,\Bigl(\mathrm{fam}(\mathcal{C},J)\wedge\forall t\,\forall D\,\bigl((t,D)\in\mathcal{C}\Rightarrow\exists y\,((t,y)\in A\wedge\forall u\,(u\in D\Leftrightarrow u=y))\bigr)\wedge\mathrm{ind}(\mathcal{F},P,J,\mathcal{C})\Bigr),$$

a predicative formula. Let sets $\Omega,\mathcal{F},P,J,A$ be assigned. The first three conjuncts hold exactly when $(\Omega,\mathcal{F},P)$ is a probability space and $A=(A_{t})_{t\in J}$ is a family of events, the events being the elements of $\mathcal{F}$ (Probability Spaces, Events and Random Elements (ii)); if they fail, $\varepsilon$ and the condition of (i) both fail. Let them hold. A set $\mathcal{C}$ satisfies the first two conjuncts inside $\exists\mathcal{C}$ exactly when it is a family indexed by $J$ with $\mathcal{C}_{t}=\{A_{t}\}$ for every $t\in J$. Such a family exists: for the predicative formula $\exists y\,((t,y)\in A\wedge\forall u\,(u\in D\Leftrightarrow u=y))$ in $t$ and $D$, with parameter $A$, every $t\in J$ has exactly one $D$ in the power set of $\mathcal{F}$ satisfying it, namely $\{A_{t}\}$, as $A_{t}\in\mathcal{F}$, so Maps from Functional Predicative Relations, and Families of Sections (ii) gives a map on $J$ with these values; and two such families are equal, having the same domain and the same values. So $\exists\mathcal{C}(\dots)$ holds if and only if $\mathrm{ind}(\mathcal{F},P,J,\mathcal{C})$ holds for the family $\mathcal{C}=(\{A_{t}\})_{t\in J}$ of subsets of $\mathcal{F}$, that is, by Step 1, if and only if this family is independent in the sense of Independence of Classes of Events and of σ-Algebras (i), that is, by Independence of Events and of Random Elements (i), if and only if $(A_{t})_{t\in J}$ is independent. Hence $\varepsilon$ expresses the condition of (i) at $\Omega,\mathcal{F},P,J,A$.

Independent random elements. Let

$$\begin{aligned} \varrho={}&\mathrm{ps}(\Omega,\mathcal{F},P)\wedge\mathrm{fam}(S,J)\wedge\mathrm{fam}(d,J)\wedge\mathrm{fam}(X,J)\wedge\forall t\,\forall s\,\forall g\,\forall v\,\bigl(((t,s)\in S\wedge(t,g)\in d\wedge(t,v)\in X)\Rightarrow\mathrm{re}(\Omega,\mathcal{F},P,s,g,v)\bigr)\\ &\wedge\exists\mathcal{C}\,\Bigl(\mathrm{fam}(\mathcal{C},J)\wedge\forall t\,\forall s\,\forall g\,\forall v\,\forall D\,\bigl(((t,s)\in S\wedge(t,g)\in d\wedge(t,v)\in X\wedge(t,D)\in\mathcal{C})\Rightarrow\mathrm{sig}(D,\Omega,s,g,v)\bigr)\wedge\mathrm{ind}(\mathcal{F},P,J,\mathcal{C})\Bigr), \end{aligned}$$

a predicative formula. Let sets $\Omega,\mathcal{F},P,J,S,d,X$ be assigned. When $S$, $d$ and $X$ are families indexed by $J$, the pairs $(t,s)\in S$, $(t,g)\in d$, $(t,v)\in X$ are those with $t\in J$, $s=S_{t}$, $g=d_{t}$ and $v=X_{t}$, so the fifth conjunct says that $\mathrm{re}(\Omega,\mathcal{F},P,S_{t},d_{t},X_{t})$ holds for every $t\in J$. Thus the first line of $\varrho$ holds exactly when every part of the condition of (ii) other than independence holds; if it fails, $\varrho$ and the condition both fail. Let it hold. Then there is exactly one family $(\sigma(X_{t}))_{t\in J}$ indexed by $J$ (Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (vi)), each $\sigma(X_{t})$ a $\sigma$-algebra on $\Omega$ contained in $\mathcal{F}$ (σ-Algebras Generated by Random Elements (i)). By Step 2, a set $\mathcal{C}$ satisfies the first two conjuncts inside $\exists\mathcal{C}$ exactly when it is a family indexed by $J$ with $\mathcal{C}_{t}=\sigma(X_{t})$ for every $t\in J$, that is, exactly when $\mathcal{C}=(\sigma(X_{t}))_{t\in J}$. So $\exists\mathcal{C}(\dots)$ holds if and only if $\mathrm{ind}$ holds for this family of subsets of $\mathcal{F}$, that is, by Step 1, if and only if it is independent as in Independence of Classes of Events and of σ-Algebras (i), which for a family of $\sigma$-algebras on $\Omega$ contained in $\mathcal{F}$ is independence as in Independence of Classes of Events and of σ-Algebras (ii), that is, by Independence of Events and of Random Elements (ii), if and only if $(X_{t})_{t\in J}$ is independent. Hence $\varrho$ expresses the condition of (ii) at $\Omega,\mathcal{F},P,J,S,d,X$.

Two independent random elements. Let

$$\pi=\mathrm{re}(\Omega,\mathcal{F},P,S,d,X)\wedge\mathrm{re}(\Omega,\mathcal{F},P,T,e,Y)\wedge\chi\bigl[\mathrm{sg}(U,\Omega,S,d,X),\mathrm{sg}(U',\Omega,T,e,Y)\bigr],$$

a predicative formula. Let sets $\Omega,\mathcal{F},P,S,d,X,T,e,Y$ be assigned. The first two conjuncts hold exactly when every part of the condition of (iii) other than independence holds; if they fail, $\pi$ and the condition both fail. Let them hold. By Step 2, the sets $U$ with $\mathrm{sg}(U,\Omega,S,d,X)$ are the elements of $\sigma(X)$, and those $U'$ with $\mathrm{sg}(U',\Omega,T,e,Y)$ the elements of $\sigma(Y)$, two $\sigma$-algebras on $\Omega$ contained in $\mathcal{F}$. By Step 3, $\chi[\dots]$ holds if and only if $P(U\cap U')=P(U)\,P(U')$ for all $U\in\sigma(X)$ and $U'\in\sigma(Y)$, that is, by Independence of Classes of Events and of σ-Algebras (iii), if and only if $\sigma(X)$ and $\sigma(Y)$ are independent, that is, by Independence of Events and of Random Elements (iii), if and only if $X$ and $Y$ are independent. Hence $\pi$ expresses the condition of (iii) at $\Omega,\mathcal{F},P,S,d,X,T,e,Y$.

A random element independent of a $\sigma$-algebra. Let

$$\theta=\mathrm{re}(\Omega,\mathcal{F},P,S,d,X)\wedge\mathrm{sa}(\mathcal{G},\Omega)\wedge\forall u\,(u\in\mathcal{G}\Rightarrow u\in\mathcal{F})\wedge\chi\bigl[\mathrm{sg}(U,\Omega,S,d,X),\,U'\in\mathcal{G}\bigr],$$

a predicative formula. Let sets $\Omega,\mathcal{F},P,S,d,X,\mathcal{G}$ be assigned. The first three conjuncts hold exactly when every part of the condition of (iv) other than independence holds, $\mathrm{sa}(\mathcal{G},\Omega)$ saying that $\mathcal{G}$ is a $\sigma$-algebra on $\Omega$; if they fail, $\theta$ and the condition both fail. Let them hold. By Step 2 the sets $U$ with $\mathrm{sg}(U,\Omega,S,d,X)$ are the elements of $\sigma(X)\subseteq\mathcal{F}$, and the sets $U'$ with $U'\in\mathcal{G}$ are elements of $\mathcal{F}$. By Step 3, $\chi[\dots]$ holds if and only if $P(U\cap U')=P(U)\,P(U')$ for all $U\in\sigma(X)$ and $U'\in\mathcal{G}$, that is, by Independence of Classes of Events and of σ-Algebras (iii), if and only if $\sigma(X)$ and $\mathcal{G}$ are independent, that is, by Independence of Events and of Random Elements (iv), if and only if $X$ is independent of $\mathcal{G}$. Hence $\theta$ expresses the condition of (iv) at $\Omega,\mathcal{F},P,S,d,X,\mathcal{G}$.

Independent and identically distributed sequences. Let

$$\begin{aligned} \kappa={}&\exists K\,\exists S'\,\exists d'\,\Bigl(\forall u\,(u\in K\Leftrightarrow u\in\mathbb{N})\wedge\mathrm{fam}(S',K)\wedge\forall h\,\forall s\,((h,s)\in S'\Rightarrow s=S)\wedge\mathrm{fam}(d',K)\wedge\forall h\,\forall g\,((h,g)\in d'\Rightarrow g=d)\wedge\varrho(\Omega,\mathcal{F},P,K,S',d',X)\Bigr)\\ &\wedge\forall h\,\forall h'\,\forall V\,\forall V'\,\bigl(((h,V)\in X\wedge(h',V')\in X)\Rightarrow\mathrm{id}(\Omega,\mathcal{F},P,S,d,V,V')\bigr), \end{aligned}$$

where $\varrho(\Omega,\mathcal{F},P,K,S',d',X)$ is the formula $\varrho$ above with $K$, $S'$, $d'$ in place of $J$, $S$, $d$; it is predicative. Let sets $\Omega,\mathcal{F},P,S,d,X$ be assigned. The sets $K$, $S'$ and $d'$ satisfying the first five conjuncts inside $\exists K\,\exists S'\,\exists d'$ are exactly $K=\mathbb{N}$, the set of natural numbers, and the constant families $S'=(S)_{n\in\mathbb{N}}$ and $d'=(d)_{n\in\mathbb{N}}$: these exist, by Maps from Functional Predicative Relations, and Families of Sections (ii) applied to the formulas $s=S$ and $g=d$ on $\mathbb{N}$ with values in $\{S\}$ and $\{d\}$, and are unique, having domain $\mathbb{N}$ and prescribed values. So, by the result for $\varrho$, the first line of $\kappa$ holds exactly when $(\Omega,\mathcal{F},P)$ is a probability space, $X=(X_{n})_{n\in\mathbb{N}}$ is a family indexed by $\mathbb{N}$, for every $n\in\mathbb{N}$, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space and $X_{n}$ is a random element of $S$, and $(X_{n})_{n\in\mathbb{N}}$ is independent as in Independence of Events and of Random Elements (ii) with $S_{n}=S$ and $d_{n}=d$ for every $n$, which is the independence that Independence of Events and of Random Elements (v) requires. As $1\in\mathbb{N}$ (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)), the requirement on $d$ and $(S,d)$ for every $n$ is the requirement on $d$ and $(S,d)$ itself. If the first line fails, $\kappa$ and the condition of (v) both fail. Let it hold. The pairs $(h,V),(h',V')\in X$ are those with $h,h'\in\mathbb{N}$, $V=X_{h}$ and $V'=X_{h'}$; for them every part of $\mathrm{id}(\Omega,\mathcal{F},P,S,d,X_{h},X_{h'})$ other than identical distribution holds, so the second line of $\kappa$ holds if and only if $X_{h}$ and $X_{h'}$ are identically distributed for all $h,h'\in\mathbb{N}$. By Independence of Events and of Random Elements (v), $\kappa$ therefore holds if and only if the condition of (v) holds at $\Omega,\mathcal{F},P,S,d,X$.

The conditions at the positions of the statement. In each of $\varepsilon$, $\varrho$, $\pi$, $\theta$ and $\kappa$, replace the named variables of the corresponding condition, simultaneously, by the variables $x_{i},x_{j},\dots$ given to them in the statement, which need not be distinct. 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), applied to the formula with its abbreviations eliminated, with the named variables as $v_{1},\dots,v_{k}$ and their positions as $y_{1},\dots,y_{k}$, the result is a predicative formula with free variables among $x_{0},\dots,x_{N-1}$ and the parameters that holds, under an assignment of sets to $x_{0},\dots,x_{N-1}$, if and only if the original formula holds with each named variable assigned the set at its position, that is, if and only if the condition holds. This proves (i), (ii), (iii), (iv) and (v).