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 𝑘 𝜑
ovnprodcl.x ( 𝜑𝑋 ∈ Fin )
ovnprodcl.f ( 𝜑𝐹 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
ovnprodcl.i ( 𝜑𝐼 ∈ ℕ )
Assertion ovnprodcl ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐹𝐼 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step Hyp Ref Expression
1 ovnprodcl.kph 𝑘 𝜑
2 ovnprodcl.x ( 𝜑𝑋 ∈ Fin )
3 ovnprodcl.f ( 𝜑𝐹 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
4 ovnprodcl.i ( 𝜑𝐼 ∈ ℕ )
5 3 4 ffvelrnd ( 𝜑 → ( 𝐹𝐼 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
6 elmapi ( ( 𝐹𝐼 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝐹𝐼 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
7 5 6 syl ( 𝜑 → ( 𝐹𝐼 ) : 𝑋 ⟶ ( ℝ × ℝ ) )
8 1 2 7 hoiprodcl ( 𝜑 → ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝐹𝐼 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )