ovolsscl

Description: If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	ovolsscl	$⊢ (A \subseteq B \land B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A) \in ℝ$

Step	Hyp	Ref	Expression
1		sstr	$⊢ (A \subseteq B \land B \subseteq ℝ) \to A \subseteq ℝ$
2	1	3adant3	$⊢ (A \subseteq B \land B \subseteq ℝ \land {vol}^{*} (B) \in ℝ) \to A \subseteq ℝ$
3		simp3	$⊢ (A \subseteq B \land B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (B) \in ℝ$
4		ovolss	$⊢ (A \subseteq B \land B \subseteq ℝ) \to {vol}^{} (A) \leq {vol}^{} (B)$
5	4	3adant3	$⊢ (A \subseteq B \land B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A) \leq {vol}^{*} (B)$
6		ovollecl	$⊢ (A \subseteq ℝ \land {vol}^{} (B) \in ℝ \land {vol}^{} (A) \leq {vol}^{} (B)) \to {vol}^{} (A) \in ℝ$
7	2 3 5 6	syl3anc	$⊢ (A \subseteq B \land B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A) \in ℝ$

Metamath Proof Explorer