Theorem omecl

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

	Ref	Expression
Hypotheses	omecl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omecl.x	⊢ 𝑋 = ∪ dom 𝑂
	omecl.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
Assertion	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		omecl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omecl.x	⊢ 𝑋 = ∪ dom 𝑂
3		omecl.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4	1 2	omef	⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
5	2	a1i	⊢ ( 𝜑 → 𝑋 = ∪ dom 𝑂 )
6	1	dmexd	⊢ ( 𝜑 → dom 𝑂 ∈ V )
7	6	uniexd	⊢ ( 𝜑 → ∪ dom 𝑂 ∈ V )
8	5 7	eqeltrd	⊢ ( 𝜑 → 𝑋 ∈ V )
9	8 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
10		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
11	9 10	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
12	3 11	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑋 )
13	4 12	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )