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	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to {vol}^{*}\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ovolcl	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)\in {ℝ}^{*}$$
2	1	3ad2ant1	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to {vol}^{*}\left(A\right)\in {ℝ}^{*}$$
3		simp2	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to B\in ℝ$$
4		ovolge0	$$⊢A\subseteq ℝ\to 0\le {vol}^{*}\left(A\right)$$
5	4	3ad2ant1	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to 0\le {vol}^{*}\left(A\right)$$
6		simp3	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to {vol}^{*}\left(A\right)\le B$$
7		xrrege0	$$⊢\left(\left({vol}^{*}\left(A\right)\in {ℝ}^{*}\wedge B\in ℝ\right)\wedge \left(0\le {vol}^{*}\left(A\right)\wedge {vol}^{*}\left(A\right)\le B\right)\right)\to {vol}^{*}\left(A\right)\in ℝ$$
8	2 3 5 6 7	syl22anc	$$⊢\left(A\subseteq ℝ\wedge B\in ℝ\wedge {vol}^{*}\left(A\right)\le B\right)\to {vol}^{*}\left(A\right)\in ℝ$$