ovnsslelem

Description: The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsslelem.1	$⊢ φ \to X \in Fin$
	ovnsslelem.2	$⊢ φ \to X \neq \emptyset$
	ovnsslelem.3	$⊢ φ \to A \subseteq B$
	ovnsslelem.4	$⊢ φ \to B \subseteq ℝ^{X}$
	ovnsslelem.5	$⊢ 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)))))\}$
	ovnsslelem.6	$⊢ N = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (B \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	ovnsslelem	$⊢ φ \to voln* (X) (A) \leq voln* (X) (B)$

Proof

Step	Hyp	Ref	Expression
1		ovnsslelem.1	$⊢ φ \to X \in Fin$
2		ovnsslelem.2	$⊢ φ \to X \neq \emptyset$
3		ovnsslelem.3	$⊢ φ \to A \subseteq B$
4		ovnsslelem.4	$⊢ φ \to B \subseteq ℝ^{X}$
5		ovnsslelem.5	$⊢ 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)))))\}$
6		ovnsslelem.6	$⊢ N = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (B \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)))))\}$
7	3	adantr	$⊢ (φ \land B \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to A \subseteq B$
8		simpr	$⊢ (φ \land B \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to B \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
9	7 8	sstrd	$⊢ (φ \land B \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
10	9	adantrr	$⊢ (φ \land (B \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 A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
11		simprr	$⊢ (φ \land (B \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 = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
12	10 11	jca	$⊢ (φ \land (B \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 (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)))))$
13	12	ex	$⊢ φ \to ((B \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 (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))))))$
14	13	reximdv	$⊢ φ \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (B \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 \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))))))$
15	14	adantr	$⊢ (φ \land z \in ℝ^{*}) \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (B \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 \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))))))$
16	15	ss2rabdv	$⊢ φ \to \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (B \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 \{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)))))\}$
17	16 6 5	3sstr4g	$⊢ φ \to N \subseteq M$
18	5	ssrab3	$⊢ M \subseteq ℝ^{*}$
19		infxrss	$⊢ (N \subseteq M \land M \subseteq ℝ^{}) \to inf (M ℝ^{} <) \leq inf (N ℝ^{*} <)$
20	17 18 19	sylancl	$⊢ φ \to inf (M ℝ^{} <) \leq inf (N ℝ^{} <)$
21	3 4	sstrd	$⊢ φ \to A \subseteq ℝ^{X}$
22	1 2 21 5	ovnn0val	$⊢ φ \to voln* (X) (A) = inf (M ℝ^{*} <)$
23	1 2 4 6	ovnn0val	$⊢ φ \to voln* (X) (B) = inf (N ℝ^{*} <)$
24	20 22 23	3brtr4d	$⊢ φ \to voln* (X) (A) \leq voln* (X) (B)$

Metamath Proof Explorer

Theorem ovnsslelem

Proof