ovolsslem

Description: Lemma for ovolss . (Contributed by Mario Carneiro, 16-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

	Ref	Expression
Hypotheses	ovolss.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
	ovolss.2	$⊢ N = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
Assertion	ovolsslem	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (B)$

Proof

Step	Hyp	Ref	Expression
1		ovolss.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
2		ovolss.2	$⊢ N = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
3		sstr2	$⊢ A \subseteq B \to (B \subseteq ⋃ ran ((.) \circ f) \to A \subseteq ⋃ ran ((.) \circ f))$
4	3	ad2antrr	$⊢ ((A \subseteq B \land B \subseteq ℝ) \land y \in ℝ^{*}) \to (B \subseteq ⋃ ran ((.) \circ f) \to A \subseteq ⋃ ran ((.) \circ f))$
5	4	anim1d	$⊢ ((A \subseteq B \land B \subseteq ℝ) \land y \in ℝ^{}) \to ((B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)))$
6	5	reximdv	$⊢ ((A \subseteq B \land B \subseteq ℝ) \land y \in ℝ^{}) \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)))$
7	6	ss2rabdv	$⊢ (A \subseteq B \land B \subseteq ℝ) \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
8	7 2 1	3sstr4g	$⊢ (A \subseteq B \land B \subseteq ℝ) \to N \subseteq M$
9		sstr	$⊢ (A \subseteq B \land B \subseteq ℝ) \to A \subseteq ℝ$
10	1	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = inf (M ℝ^{} <)$
11	10	adantr	$⊢ (A \subseteq ℝ \land x \in M) \to {vol}^{} (A) = inf (M ℝ^{} <)$
12	1	ssrab3	$⊢ M \subseteq ℝ^{*}$
13		infxrlb	$⊢ (M \subseteq ℝ^{} \land x \in M) \to inf (M ℝ^{} <) \leq x$
14	12 13	mpan	$⊢ x \in M \to inf (M ℝ^{*} <) \leq x$
15	14	adantl	$⊢ (A \subseteq ℝ \land x \in M) \to inf (M ℝ^{*} <) \leq x$
16	11 15	eqbrtrd	$⊢ (A \subseteq ℝ \land x \in M) \to {vol}^{*} (A) \leq x$
17	16	ralrimiva	$⊢ A \subseteq ℝ \to \forall x \in M {vol}^{*} (A) \leq x$
18	9 17	syl	$⊢ (A \subseteq B \land B \subseteq ℝ) \to \forall x \in M {vol}^{*} (A) \leq x$
19		ssralv	$⊢ N \subseteq M \to (\forall x \in M {vol}^{} (A) \leq x \to \forall x \in N {vol}^{} (A) \leq x)$
20	8 18 19	sylc	$⊢ (A \subseteq B \land B \subseteq ℝ) \to \forall x \in N {vol}^{*} (A) \leq x$
21	2	ssrab3	$⊢ N \subseteq ℝ^{*}$
22		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
23	9 22	syl	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \in ℝ^{}$
24		infxrgelb	$⊢ (N \subseteq ℝ^{} \land {vol}^{} (A) \in ℝ^{}) \to ({vol}^{} (A) \leq inf (N ℝ^{} <) \leftrightarrow \forall x \in N {vol}^{} (A) \leq x)$
25	21 23 24	sylancr	$⊢ (A \subseteq B \land B \subseteq ℝ) \to ({vol}^{} (A) \leq inf (N ℝ^{} <) \leftrightarrow \forall x \in N {vol}^{*} (A) \leq x)$
26	20 25	mpbird	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq inf (N ℝ^{} <)$
27	2	ovolval	$⊢ B \subseteq ℝ \to {vol}^{} (B) = inf (N ℝ^{} <)$
28	27	adantl	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (B) = inf (N ℝ^{} <)$
29	26 28	breqtrrd	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (B)$

Metamath Proof Explorer

Theorem ovolsslem

Proof