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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omessre.x	⊢ 𝑋 = ∪ dom 𝑂
	omessre.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
	omessre.re	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
	omessre.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	omessre	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		omessre.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omessre.x	⊢ 𝑋 = ∪ dom 𝑂
3		omessre.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		omessre.re	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
5		omessre.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
6		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
7		0xr	⊢ 0 ∈ ℝ^*
8	7	a1i	⊢ ( 𝜑 → 0 ∈ ℝ^* )
9		pnfxr	⊢ +∞ ∈ ℝ^*
10	9	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
11	5 3	sstrd	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
12	1 2 11	omexrcl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ℝ^* )
13	1 2 11	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
14		iccgelb	⊢ ( ( 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ ( 𝑂 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑂 ‘ 𝐵 ) )
15	8 10 13 14	syl3anc	⊢ ( 𝜑 → 0 ≤ ( 𝑂 ‘ 𝐵 ) )
16	4	rexrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ^* )
17	1 2 3 5	omessle	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ≤ ( 𝑂 ‘ 𝐴 ) )
18	4	ltpnfd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) < +∞ )
19	12 16 10 17 18	xrlelttrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) < +∞ )
20	8 10 12 15 19	elicod	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) )
21	6 20	sselid	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ℝ )

Metamath Proof Explorer

Theorem omessre

Proof