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 
|- ( ph -> O e. OutMeas )
omessre.x 
|- X = U. dom O
omessre.a 
|- ( ph -> A C_ X )
omessre.re 
|- ( ph -> ( O ` A ) e. RR )
omessre.b 
|- ( ph -> B C_ A )
Assertion omessre 
|- ( ph -> ( O ` B ) e. RR )

Proof

Step Hyp Ref Expression
1 omessre.o 
 |-  ( ph -> O e. OutMeas )
2 omessre.x 
 |-  X = U. dom O
3 omessre.a 
 |-  ( ph -> A C_ X )
4 omessre.re 
 |-  ( ph -> ( O ` A ) e. RR )
5 omessre.b 
 |-  ( ph -> B C_ A )
6 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
7 0xr 
 |-  0 e. RR*
8 7 a1i 
 |-  ( ph -> 0 e. RR* )
9 pnfxr 
 |-  +oo e. RR*
10 9 a1i 
 |-  ( ph -> +oo e. RR* )
11 5 3 sstrd 
 |-  ( ph -> B C_ X )
12 1 2 11 omexrcl 
 |-  ( ph -> ( O ` B ) e. RR* )
13 1 2 11 omecl 
 |-  ( ph -> ( O ` B ) e. ( 0 [,] +oo ) )
14 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( O ` B ) e. ( 0 [,] +oo ) ) -> 0 <_ ( O ` B ) )
15 8 10 13 14 syl3anc 
 |-  ( ph -> 0 <_ ( O ` B ) )
16 4 rexrd 
 |-  ( ph -> ( O ` A ) e. RR* )
17 1 2 3 5 omessle 
 |-  ( ph -> ( O ` B ) <_ ( O ` A ) )
18 4 ltpnfd 
 |-  ( ph -> ( O ` A ) < +oo )
19 12 16 10 17 18 xrlelttrd 
 |-  ( ph -> ( O ` B ) < +oo )
20 8 10 12 15 19 elicod 
 |-  ( ph -> ( O ` B ) e. ( 0 [,) +oo ) )
21 6 20 sseldi 
 |-  ( ph -> ( O ` B ) e. RR )