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 ( 𝜑𝑂 ∈ OutMeas )
omexrcl.x 𝑋 = dom 𝑂
omexrcl.a ( 𝜑𝐴𝑋 )
Assertion omexrcl ( 𝜑 → ( 𝑂𝐴 ) ∈ ℝ* )

Proof

Step Hyp Ref Expression
1 omexrcl.o ( 𝜑𝑂 ∈ OutMeas )
2 omexrcl.x 𝑋 = dom 𝑂
3 omexrcl.a ( 𝜑𝐴𝑋 )
4 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
5 1 2 3 omecl ( 𝜑 → ( 𝑂𝐴 ) ∈ ( 0 [,] +∞ ) )
6 4 5 sseldi ( 𝜑 → ( 𝑂𝐴 ) ∈ ℝ* )