Metamath Proof Explorer


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 φ O OutMeas
omess0.x X = dom O
omess0.a φ A X
omess0.z φ O A = 0
omess0.s φ B A
Assertion omess0 φ O B = 0

Proof

Step Hyp Ref Expression
1 omess0.o φ O OutMeas
2 omess0.x X = dom O
3 omess0.a φ A X
4 omess0.z φ O A = 0
5 omess0.s φ B A
6 5 3 sstrd φ B X
7 1 2 6 omexrcl φ O B *
8 0xr 0 *
9 8 a1i φ 0 *
10 1 2 3 5 omessle φ O B O A
11 10 4 breqtrd φ O B 0
12 1 2 6 omege0 φ 0 O B
13 7 9 11 12 xrletrid φ O B = 0