Theorem omess0

Description: If the outer measure of a set is 0 , then the outer measure of its subsets is 0 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	omess0.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omess0.x	⊢ 𝑋 = ∪ dom 𝑂
	omess0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
	omess0.z	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 0 )
	omess0.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	omess0	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		omess0.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omess0.x	⊢ 𝑋 = ∪ dom 𝑂
3		omess0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		omess0.z	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 0 )
5		omess0.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
6	5 3	sstrd	⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
7	1 2 6	omexrcl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ∈ ℝ* )
8		0xr	⊢ 0 ∈ ℝ*
9	8	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
10	1 2 3 5	omessle	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ≤ ( 𝑂 ‘ 𝐴 ) )
11	10 4	breqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) ≤ 0 )
12	1 2 6	omege0	⊢ ( 𝜑 → 0 ≤ ( 𝑂 ‘ 𝐵 ) )
13	7 9 11 12	xrletrid	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) = 0 )