# Metamath Proof Explorer

## Theorem ovolssnul

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

Ref Expression
Assertion ovolssnul ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({A}\right)=0$

### Proof

Step Hyp Ref Expression
1 ovolss ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\right)\to {vol}^{*}\left({A}\right)\le {vol}^{*}\left({B}\right)$
2 1 3adant3 ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({A}\right)\le {vol}^{*}\left({B}\right)$
3 simp3 ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({B}\right)=0$
4 2 3 breqtrd ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({A}\right)\le 0$
5 sstr ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\right)\to {A}\subseteq ℝ$
6 5 3adant3 ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {A}\subseteq ℝ$
7 ovolge0 ${⊢}{A}\subseteq ℝ\to 0\le {vol}^{*}\left({A}\right)$
8 6 7 syl ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to 0\le {vol}^{*}\left({A}\right)$
9 ovolcl ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
10 6 9 syl ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
11 0xr ${⊢}0\in {ℝ}^{*}$
12 xrletri3 ${⊢}\left({vol}^{*}\left({A}\right)\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left({vol}^{*}\left({A}\right)=0↔\left({vol}^{*}\left({A}\right)\le 0\wedge 0\le {vol}^{*}\left({A}\right)\right)\right)$
13 10 11 12 sylancl ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to \left({vol}^{*}\left({A}\right)=0↔\left({vol}^{*}\left({A}\right)\le 0\wedge 0\le {vol}^{*}\left({A}\right)\right)\right)$
14 4 8 13 mpbir2and ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)=0\right)\to {vol}^{*}\left({A}\right)=0$