Metamath Proof Explorer

Theorem ovolun

Description: The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun , this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land x \in ℝ^{+}) \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
2		simplr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land x \in ℝ^{+}) \to (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ)$
3		simpr	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
4	1 2 3	ovolunlem2	$⊢ (((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \land x \in ℝ^{+}) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + x$
5	4	ralrimiva	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to \forall x \in ℝ^{+} {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + x$
6		unss	$⊢ (A \subseteq ℝ \land B \subseteq ℝ) \leftrightarrow A \cup B \subseteq ℝ$
7	6	biimpi	$⊢ (A \subseteq ℝ \land B \subseteq ℝ) \to A \cup B \subseteq ℝ$
8	7	ad2ant2r	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to A \cup B \subseteq ℝ$
9		ovolcl	$⊢ A \cup B \subseteq ℝ \to {vol}^{} (A \cup B) \in ℝ^{}$
10	8 9	syl	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) \in ℝ^{}$
11		readdcl	$⊢ ({vol}^{} (A) \in ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
12	11	ad2ant2l	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
13		xralrple	$⊢ ({vol}^{} (A \cup B) \in ℝ^{} \land {vol}^{} (A) + {vol}^{} (B) \in ℝ) \to ({vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B) + x)$
14	10 12 13	syl2anc	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to ({vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{} (B) + x)$
15	5 14	mpbird	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ) \land (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B)$