Theorem 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	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
2	1	3adant3	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → 𝐴 ⊆ ℝ )
3		simp3	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐵 ) ∈ ℝ )
4		ovolss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )
5	4	3adant3	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )
6		ovollecl	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
7	2 3 5 6	syl3anc	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )