Theorem ovollecl

Description: If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014)

	Ref	Expression
Assertion	ovollecl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ovolcl	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
2	1	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
3		simp2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → 𝐵 ∈ ℝ )
4		ovolge0	⊢ ( 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝐴 ) )
5	4	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → 0 ≤ ( vol* ‘ 𝐴 ) )
6		simp3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ≤ 𝐵 )
7		xrrege0	⊢ ( ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ ( vol* ‘ 𝐴 ) ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
8	2 3 5 6 7	syl22anc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ )