Theorem omege0

Description: If the outer measure of a set is greater than or equal to 0 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	omege0.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omege0.x	⊢ 𝑋 = ∪ dom 𝑂
	omege0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
Assertion	omege0	⊢ ( 𝜑 → 0 ≤ ( 𝑂 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		omege0.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omege0.x	⊢ 𝑋 = ∪ dom 𝑂
3		omege0.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		0xr	⊢ 0 ∈ ℝ*
5	4	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
6		pnfxr	⊢ +∞ ∈ ℝ*
7	6	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
8	1 2 3	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
9		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝑂 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑂 ‘ 𝐴 ) )
10	5 7 8 9	syl3anc	⊢ ( 𝜑 → 0 ≤ ( 𝑂 ‘ 𝐴 ) )