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\phi$$
	ovnprodcl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnprodcl.f	$$⊢\phi \to F:\mathbb{N}⟶{{ℝ}^2}^X$$
	ovnprodcl.i	$$⊢\phi \to I\in \mathbb{N}$$
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\phi$$
2		ovnprodcl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
3		ovnprodcl.f	$$⊢\phi \to F:\mathbb{N}⟶{{ℝ}^2}^X$$
4		ovnprodcl.i	$$⊢\phi \to I\in \mathbb{N}$$
5	3 4	ffvelcdmd	$$⊢\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)$$