ovollecl

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

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

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

Metamath Proof Explorer