Metamath Proof Explorer

Theorem ovolssnul

Description: A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion ovolssnul ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 ovolss ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )
2 1 3adant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )
3 simp3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐵 ) = 0 )
4 2 3 breqtrd ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) ≤ 0 )
5 sstr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
6 5 3adant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → 𝐴 ⊆ ℝ )
7 ovolge0 ⊢ ( 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝐴 ) )
8 6 7 syl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → 0 ≤ ( vol* ‘ 𝐴 ) )
9 ovolcl ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
10 6 9 syl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
11 0xr ⊢ 0 ∈ ℝ*
12 xrletri3 ⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol* ‘ 𝐴 ) = 0 ↔ ( ( vol* ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ 𝐴 ) ) ) )
13 10 11 12 sylancl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( ( vol* ‘ 𝐴 ) = 0 ↔ ( ( vol* ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( vol* ‘ 𝐴 ) ) ) )
14 4 8 13 mpbir2and ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) = 0 ) → ( vol* ‘ 𝐴 ) = 0 )