ovnsupge0

Description: The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsupge0.1	$⊢ φ \to X \in Fin$
	ovnsupge0.2	$⊢ φ \to A \subseteq ℝ^{X}$
	ovnsupge0.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
Assertion	ovnsupge0	$⊢ φ \to M \subseteq [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		ovnsupge0.1	$⊢ φ \to X \in Fin$
2		ovnsupge0.2	$⊢ φ \to A \subseteq ℝ^{X}$
3		ovnsupge0.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
4		simp3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
5		nnex	$⊢ ℕ \in V$
6	5	a1i	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to ℕ \in V$
7		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
8		nfv	$⊢ Ⅎ k ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ)$
9	1	ad2antrr	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ) \to X \in Fin$
10		elmapi	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to i : ℕ ⟶ {ℝ^{2}}^{X}$
11	10	ad2antlr	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ) \to i : ℕ ⟶ {ℝ^{2}}^{X}$
12		simpr	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ) \to j \in ℕ$
13	8 9 11 12	ovnprodcl	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) \in [0, +∞)$
14	7 13	sseldi	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) \in [0, +∞]$
15		eqid	$⊢ (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
16	14 15	fmptd	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))) : ℕ ⟶ [0, +∞]$
17	6 16	sge0cl	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \in [0, +∞]$
18	17	3adant3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \in [0, +∞]$
19	4 18	eqeltrd	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞]$
20	19	3adant3l	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))) \to z \in [0, +∞]$
21	20	3exp	$⊢ φ \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞]))$
22	21	adantr	$⊢ (φ \land z \in ℝ^{*}) \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞]))$
23	22	rexlimdv	$⊢ (φ \land z \in ℝ^{*}) \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞])$
24	23	ralrimiva	$⊢ φ \to \forall z \in ℝ^{*} (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞])$
25		rabss	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \subseteq [0, +∞] \leftrightarrow \forall z \in ℝ^{} (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \in [0, +∞])$
26	24 25	sylibr	$⊢ φ \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \subseteq [0, +∞]$
27	3 26	eqsstrid	$⊢ φ \to M \subseteq [0, +∞]$

Metamath Proof Explorer

Theorem ovnsupge0

Proof