omessre

Description: If the outer measure of a set is real, then the outer measure of any of its subset is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omessre.o	$⊢ φ \to O \in OutMeas$
	omessre.x	$⊢ X = ⋃ dom O$
	omessre.a	$⊢ φ \to A \subseteq X$
	omessre.re	$⊢ φ \to O (A) \in ℝ$
	omessre.b	$⊢ φ \to B \subseteq A$
Assertion	omessre	$⊢ φ \to O (B) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		omessre.o	$⊢ φ \to O \in OutMeas$
2		omessre.x	$⊢ X = ⋃ dom O$
3		omessre.a	$⊢ φ \to A \subseteq X$
4		omessre.re	$⊢ φ \to O (A) \in ℝ$
5		omessre.b	$⊢ φ \to B \subseteq A$
6		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
7		0xr	$⊢ 0 \in ℝ^{*}$
8	7	a1i	$⊢ φ \to 0 \in ℝ^{*}$
9		pnfxr	$⊢ +∞ \in ℝ^{*}$
10	9	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
11	5 3	sstrd	$⊢ φ \to B \subseteq X$
12	1 2 11	omexrcl	$⊢ φ \to O (B) \in ℝ^{*}$
13	1 2 11	omecl	$⊢ φ \to O (B) \in [0, +∞]$
14		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land O (B) \in [0, +∞]) \to 0 \leq O (B)$
15	8 10 13 14	syl3anc	$⊢ φ \to 0 \leq O (B)$
16	4	rexrd	$⊢ φ \to O (A) \in ℝ^{*}$
17	1 2 3 5	omessle	$⊢ φ \to O (B) \leq O (A)$
18	4	ltpnfd	$⊢ φ \to O (A) < +∞$
19	12 16 10 17 18	xrlelttrd	$⊢ φ \to O (B) < +∞$
20	8 10 12 15 19	elicod	$⊢ φ \to O (B) \in [0, +∞)$
21	6 20	sseldi	$⊢ φ \to O (B) \in ℝ$

Metamath Proof Explorer

Theorem omessre

Proof