# Metamath Proof Explorer

## Theorem ovnprodcl

Description: The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnprodcl.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
ovnprodcl.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
ovnprodcl.f ${⊢}{\phi }\to {F}:ℕ⟶{{ℝ}^{2}}^{{X}}$
ovnprodcl.i ${⊢}{\phi }\to {I}\in ℕ$
Assertion ovnprodcl ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {F}\left({I}\right)\right)\left({k}\right)\right)\in \left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 ovnprodcl.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 ovnprodcl.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
3 ovnprodcl.f ${⊢}{\phi }\to {F}:ℕ⟶{{ℝ}^{2}}^{{X}}$
4 ovnprodcl.i ${⊢}{\phi }\to {I}\in ℕ$
5 3 4 ffvelrnd ${⊢}{\phi }\to {F}\left({I}\right)\in \left({{ℝ}^{2}}^{{X}}\right)$
6 elmapi ${⊢}{F}\left({I}\right)\in \left({{ℝ}^{2}}^{{X}}\right)\to {F}\left({I}\right):{X}⟶{ℝ}^{2}$
7 5 6 syl ${⊢}{\phi }\to {F}\left({I}\right):{X}⟶{ℝ}^{2}$
8 1 2 7 hoiprodcl ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {F}\left({I}\right)\right)\left({k}\right)\right)\in \left[0,\mathrm{+\infty }\right)$