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	|- ( ph -> O e. OutMeas )
	omess0.x	|- X = U. dom O
	omess0.a	|- ( ph -> A C_ X )
	omess0.z	|- ( ph -> ( O ` A ) = 0 )
	omess0.s	|- ( ph -> B C_ A )
Assertion	omess0	|- ( ph -> ( O ` B ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		omess0.o	|- ( ph -> O e. OutMeas )
2		omess0.x	|- X = U. dom O
3		omess0.a	|- ( ph -> A C_ X )
4		omess0.z	|- ( ph -> ( O ` A ) = 0 )
5		omess0.s	|- ( ph -> B C_ A )
6	5 3	sstrd	|- ( ph -> B C_ X )
7	1 2 6	omexrcl	|- ( ph -> ( O ` B ) e. RR* )
8		0xr	|- 0 e. RR*
9	8	a1i	|- ( ph -> 0 e. RR* )
10	1 2 3 5	omessle	|- ( ph -> ( O ` B ) <_ ( O ` A ) )
11	10 4	breqtrd	|- ( ph -> ( O ` B ) <_ 0 )
12	1 2 6	omege0	|- ( ph -> 0 <_ ( O ` B ) )
13	7 9 11 12	xrletrid	|- ( ph -> ( O ` B ) = 0 )