hoiprodcl2

Description: The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Step	Hyp	Ref	Expression
1		hoiprodcl2.kph	$⊢ Ⅎ k φ$
2		hoiprodcl2.x	$⊢ φ \to X \in Fin$
3		hoiprodcl2.l	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
4		hoiprodcl2.i	$⊢ φ \to I : X ⟶ ℝ^{2}$
5		coeq2	$⊢ i = I \to [.) \circ i = [.) \circ I$
6	5	fveq1d	$⊢ i = I \to ([.) \circ i) (k) = ([.) \circ I) (k)$
7	6	fveq2d	$⊢ i = I \to vol (([.) \circ i) (k)) = vol (([.) \circ I) (k))$
8	7	ralrimivw	$⊢ i = I \to \forall k \in X vol (([.) \circ i) (k)) = vol (([.) \circ I) (k))$
9	8	prodeq2d	$⊢ i = I \to \prod_{k \in X} vol (([.) \circ i) (k)) = \prod_{k \in X} vol (([.) \circ I) (k))$
10		reex	$⊢ ℝ \in V$
11	10 10	xpex	$⊢ ℝ^{2} \in V$
12	11	a1i	$⊢ φ \to ℝ^{2} \in V$
13	12 2	jca	$⊢ φ \to (ℝ^{2} \in V \land X \in Fin)$
14		elmapg	$⊢ (ℝ^{2} \in V \land X \in Fin) \to (I \in ({ℝ^{2}}^{X}) \leftrightarrow I : X ⟶ ℝ^{2})$
15	13 14	syl	$⊢ φ \to (I \in ({ℝ^{2}}^{X}) \leftrightarrow I : X ⟶ ℝ^{2})$
16	4 15	mpbird	$⊢ φ \to I \in ({ℝ^{2}}^{X})$
17	1 2 4	hoiprodcl	$⊢ φ \to \prod_{k \in X} vol (([.) \circ I) (k)) \in [0, +∞)$
18	3 9 16 17	fvmptd3	$⊢ φ \to L (I) = \prod_{k \in X} vol (([.) \circ I) (k))$
19	18 17	eqeltrd	$⊢ φ \to L (I) \in [0, +∞)$

Metamath Proof Explorer