Metamath Proof Explorer

Theorem volss

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

Ref Expression
Assertion volss ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → vol ⁡ A ≤ vol ⁡ B

Proof

Step Hyp Ref Expression
1 simp3 ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → A ⊆ B
2 mblss ⊢ B ∈ dom ⁡ vol → B ⊆ ℝ
3 2 3ad2ant2 ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → B ⊆ ℝ
4 ovolss ⊢ A ⊆ B ∧ B ⊆ ℝ → vol * ⁡ A ≤ vol * ⁡ B
5 1 3 4 syl2anc ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → vol * ⁡ A ≤ vol * ⁡ B
6 mblvol ⊢ A ∈ dom ⁡ vol → vol ⁡ A = vol * ⁡ A
7 6 3ad2ant1 ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → vol ⁡ A = vol * ⁡ A
8 mblvol ⊢ B ∈ dom ⁡ vol → vol ⁡ B = vol * ⁡ B
9 8 3ad2ant2 ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → vol ⁡ B = vol * ⁡ B
10 5 7 9 3brtr4d ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol ∧ A ⊆ B → vol ⁡ A ≤ vol ⁡ B