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\leftrightarrow \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\leftrightarrow \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$$