Metamath Proof Explorer


Theorem omexrcl

Description: The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omexrcl.o
|- ( ph -> O e. OutMeas )
omexrcl.x
|- X = U. dom O
omexrcl.a
|- ( ph -> A C_ X )
Assertion omexrcl
|- ( ph -> ( O ` A ) e. RR* )

Proof

Step Hyp Ref Expression
1 omexrcl.o
 |-  ( ph -> O e. OutMeas )
2 omexrcl.x
 |-  X = U. dom O
3 omexrcl.a
 |-  ( ph -> A C_ X )
4 iccssxr
 |-  ( 0 [,] +oo ) C_ RR*
5 1 2 3 omecl
 |-  ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )
6 4 5 sseldi
 |-  ( ph -> ( O ` A ) e. RR* )