Theorem ovnome

Description: ( voln*X ) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X . Proposition 115D (a) of Fremlin1 p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	ovnome.1	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$

Proof

Step	Hyp	Ref	Expression
1		ovnome.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovexd	$$⊢\phi \to {ℝ}^X\in \mathrm{V}$$
3	1	ovnf	$$⊢\phi \to \mathrm{voln*}\left(X\right):𝒫\left({ℝ}^X\right)⟶\left[0,\mathrm{+\infty }\right]$$
4	1	ovn0	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(\varnothing \right)=0$$
5	1	3ad2ant1	$$⊢\left(\phi \wedge x\subseteq {ℝ}^X\wedge y\subseteq x\right)\to X\in \mathrm{Fin}$$
6		simp3	$$⊢\left(\phi \wedge x\subseteq {ℝ}^X\wedge y\subseteq x\right)\to y\subseteq x$$
7		simp2	$$⊢\left(\phi \wedge x\subseteq {ℝ}^X\wedge y\subseteq x\right)\to x\subseteq {ℝ}^X$$
8	5 6 7	ovnssle	$$⊢\left(\phi \wedge x\subseteq {ℝ}^X\wedge y\subseteq x\right)\to \mathrm{voln*}\left(X\right)\left(y\right)\le \mathrm{voln*}\left(X\right)\left(x\right)$$
9	1	adantr	$$⊢\left(\phi \wedge a:\mathbb{N}⟶𝒫\left({ℝ}^X\right)\right)\to X\in \mathrm{Fin}$$
10		simpr	$$⊢\left(\phi \wedge a:\mathbb{N}⟶𝒫\left({ℝ}^X\right)\right)\to a:\mathbb{N}⟶𝒫\left({ℝ}^X\right)$$
11	9 10	ovnsubadd	$$⊢\left(\phi \wedge a:\mathbb{N}⟶𝒫\left({ℝ}^X\right)\right)\to \mathrm{voln*}\left(X\right)\left(\bigcup _{n\in \mathbb{N}}a\left(n\right)\right)\le \mathrm{sum^}\left(\left(n\in \mathbb{N}⟼\mathrm{voln*}\left(X\right)\left(a\left(n\right)\right)\right)\right)$$
12	2 3 4 8 11	isomennd	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$