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	|- ( ph -> M e. Meas )
	meage0.a	|- ( ph -> A e. dom M )
Assertion	meage0	|- ( ph -> 0 <_ ( M ` A ) )

Proof

Step	Hyp	Ref	Expression
1		meage0.m	|- ( ph -> M e. Meas )
2		meage0.a	|- ( ph -> A e. dom M )
3		0xr	|- 0 e. RR*
4	3	a1i	|- ( ph -> 0 e. RR* )
5		pnfxr	|- +oo e. RR*
6	5	a1i	|- ( ph -> +oo e. RR* )
7		eqid	|- dom M = dom M
8	1 7 2	meacl	|- ( ph -> ( M ` A ) e. ( 0 [,] +oo ) )
9		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ ( M ` A ) e. ( 0 [,] +oo ) ) -> 0 <_ ( M ` A ) )
10	4 6 8 9	syl3anc	|- ( ph -> 0 <_ ( M ` A ) )