ovolss

Description: The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Assertion	ovolss	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (B)$

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

Metamath Proof Explorer