Theorem meage0

Description: If the measure of a measurable set is greater than or equal to 0 . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meage0.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meage0.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
Assertion	meage0	⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		meage0.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meage0.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
3		0xr	⊢ 0 ∈ ℝ*
4	3	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6	5	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
7		eqid	⊢ dom 𝑀 = dom 𝑀
8	1 7 2	meacl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
9		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑀 ‘ 𝐴 ) )
10	4 6 8 9	syl3anc	⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ 𝐴 ) )