ovnf

Description: The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypothesis	ovnf.1	$⊢ φ \to X \in Fin$
	Assertion	ovnf	$⊢ φ \to voln* (X) : 𝒫 (ℝ^{X}) ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		ovnf.1	$⊢ φ \to X \in Fin$
2		0e0iccpnf	$⊢ 0 \in [0, +∞]$
3	2	a1i	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to 0 \in [0, +∞]$
4		0xr	$⊢ 0 \in ℝ^{*}$
5	4	a1i	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to 0 \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7	6	a1i	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to +∞ \in ℝ^{*}$
8	1	adantr	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to X \in Fin$
9		elpwi	$⊢ y \in 𝒫 (ℝ^{X}) \to y \subseteq ℝ^{X}$
10	9	adantl	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to y \subseteq ℝ^{X}$
11		eqid	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\}$
12	8 10 11	ovnsupge0	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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, +∞]$
13	8 10 11	ovnpnfelsup	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to +∞ \in \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\}$
14	13	ne0d	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} \neq \emptyset$
15	5 7 12 14	inficc	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <) \in [0, +∞]$
16	3 15	ifcld	$⊢ (φ \land y \in 𝒫 (ℝ^{X})) \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)) \in [0, +∞]$
17		eqid	$⊢ (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <))) = (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)))$
18	16 17	fmptd	$⊢ φ \to (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <))) : 𝒫 (ℝ^{X}) ⟶ [0, +∞]$
19	1	ovnval	$⊢ φ \to voln* (X) = (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)))$
20	19	feq1d	$⊢ φ \to (voln* (X) : 𝒫 (ℝ^{X}) ⟶ [0, +∞] \leftrightarrow (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <))) : 𝒫 (ℝ^{X}) ⟶ [0, +∞])$
21	18 20	mpbird	$⊢ φ \to voln* (X) : 𝒫 (ℝ^{X}) ⟶ [0, +∞]$

Metamath Proof Explorer

Theorem ovnf

Proof