Metamath Proof Explorer


Theorem 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 φOOutMeas
omessre.x X=domO
omessre.a φAX
omessre.re φOA
omessre.b φBA
Assertion omessre φOB

Proof

Step Hyp Ref Expression
1 omessre.o φOOutMeas
2 omessre.x X=domO
3 omessre.a φAX
4 omessre.re φOA
5 omessre.b φBA
6 rge0ssre 0+∞
7 0xr 0*
8 7 a1i φ0*
9 pnfxr +∞*
10 9 a1i φ+∞*
11 5 3 sstrd φBX
12 1 2 11 omexrcl φOB*
13 1 2 11 omecl φOB0+∞
14 iccgelb 0*+∞*OB0+∞0OB
15 8 10 13 14 syl3anc φ0OB
16 4 rexrd φOA*
17 1 2 3 5 omessle φOBOA
18 4 ltpnfd φOA<+∞
19 12 16 10 17 18 xrlelttrd φOB<+∞
20 8 10 12 15 19 elicod φOB0+∞
21 6 20 sselid φOB