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	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	omess0.x	$$⊢X=\bigcup \mathrm{dom}O$$
	omess0.a	$$⊢\phi \to A\subseteq X$$
	omess0.z	$$⊢\phi \to O\left(A\right)=0$$
	omess0.s	$$⊢\phi \to B\subseteq A$$
Assertion	omess0	$$⊢\phi \to O\left(B\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		omess0.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		omess0.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		omess0.a	$$⊢\phi \to A\subseteq X$$
4		omess0.z	$$⊢\phi \to O\left(A\right)=0$$
5		omess0.s	$$⊢\phi \to B\subseteq A$$
6	5 3	sstrd	$$⊢\phi \to B\subseteq X$$
7	1 2 6	omexrcl	$$⊢\phi \to O\left(B\right)\in {ℝ}^{*}$$
8		0xr	$$⊢0\in {ℝ}^{*}$$
9	8	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
10	1 2 3 5	omessle	$$⊢\phi \to O\left(B\right)\le O\left(A\right)$$
11	10 4	breqtrd	$$⊢\phi \to O\left(B\right)\le 0$$
12	1 2 6	omege0	$$⊢\phi \to 0\le O\left(B\right)$$
13	7 9 11 12	xrletrid	$$⊢\phi \to O\left(B\right)=0$$