This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ 𝐴 ⊆ 𝐵 ) → ( vol ‘ 𝐴 ) ≤ ( vol ‘ 𝐵 ) )

Proof

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