volss

Description: The Lebesgue measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 17-Oct-2017)

		Ref	Expression
	Assertion	volss	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to vol (A) \leq vol (B)$

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to A \subseteq B$
2		mblss	$⊢ B \in dom vol \to B \subseteq ℝ$
3	2	3ad2ant2	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to B \subseteq ℝ$
4		ovolss	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (B)$
5	1 3 4	syl2anc	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to {vol}^{} (A) \leq {vol}^{} (B)$
6		mblvol	$⊢ A \in dom vol \to vol (A) = {vol}^{*} (A)$
7	6	3ad2ant1	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to vol (A) = {vol}^{*} (A)$
8		mblvol	$⊢ B \in dom vol \to vol (B) = {vol}^{*} (B)$
9	8	3ad2ant2	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to vol (B) = {vol}^{*} (B)$
10	5 7 9	3brtr4d	$⊢ (A \in dom vol \land B \in dom vol \land A \subseteq B) \to vol (A) \leq vol (B)$

Metamath Proof Explorer