This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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* ‘ 𝐴 ) ∈ ℝ )