ovolssnul

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

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

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

Metamath Proof Explorer