ovnssle

Description: The (multidimensional) 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	ovnssle.1	$⊢ φ \to X \in Fin$
	ovnssle.2	$⊢ φ \to A \subseteq B$
	ovnssle.3	$⊢ φ \to B \subseteq ℝ^{X}$
Assertion	ovnssle	$⊢ φ \to voln* (X) (A) \leq voln* (X) (B)$

Proof

Step	Hyp	Ref	Expression
1		ovnssle.1	$⊢ φ \to X \in Fin$
2		ovnssle.2	$⊢ φ \to A \subseteq B$
3		ovnssle.3	$⊢ φ \to B \subseteq ℝ^{X}$
4		0le0	$⊢ 0 \leq 0$
5	4	a1i	$⊢ (φ \land X = \emptyset) \to 0 \leq 0$
6		fveq2	$⊢ X = \emptyset \to voln* (X) = voln* (\emptyset)$
7	6	fveq1d	$⊢ X = \emptyset \to voln* (X) (A) = voln* (\emptyset) (A)$
8	7	adantl	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) = voln* (\emptyset) (A)$
9	2	adantr	$⊢ (φ \land X = \emptyset) \to A \subseteq B$
10	3	adantr	$⊢ (φ \land X = \emptyset) \to B \subseteq ℝ^{X}$
11		simpr	$⊢ (φ \land X = \emptyset) \to X = \emptyset$
12	11	oveq2d	$⊢ (φ \land X = \emptyset) \to ℝ^{X} = ℝ^{\emptyset}$
13	10 12	sseqtrd	$⊢ (φ \land X = \emptyset) \to B \subseteq ℝ^{\emptyset}$
14	9 13	sstrd	$⊢ (φ \land X = \emptyset) \to A \subseteq ℝ^{\emptyset}$
15	14	ovn0val	$⊢ (φ \land X = \emptyset) \to voln* (\emptyset) (A) = 0$
16	8 15	eqtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) = 0$
17	6	fveq1d	$⊢ X = \emptyset \to voln* (X) (B) = voln* (\emptyset) (B)$
18	17	adantl	$⊢ (φ \land X = \emptyset) \to voln* (X) (B) = voln* (\emptyset) (B)$
19	13	ovn0val	$⊢ (φ \land X = \emptyset) \to voln* (\emptyset) (B) = 0$
20	18 19	eqtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (B) = 0$
21	16 20	breq12d	$⊢ (φ \land X = \emptyset) \to (voln* (X) (A) \leq voln* (X) (B) \leftrightarrow 0 \leq 0)$
22	5 21	mpbird	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) \leq voln* (X) (B)$
23	1	adantr	$⊢ (φ \land \neg X = \emptyset) \to X \in Fin$
24		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
25	24	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
26	2	adantr	$⊢ (φ \land \neg X = \emptyset) \to A \subseteq B$
27	3	adantr	$⊢ (φ \land \neg X = \emptyset) \to B \subseteq ℝ^{X}$
28		eqid	$⊢ \{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)))))\} = \{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)))))\}$
29		eqid	$⊢ \{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)))))\} = \{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)))))\}$
30	23 25 26 27 28 29	ovnsslelem	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (A) \leq voln* (X) (B)$
31	22 30	pm2.61dan	$⊢ φ \to voln* (X) (A) \leq voln* (X) (B)$

Metamath Proof Explorer

Theorem ovnssle

Proof