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	|- ( ph -> O e. OutMeas )
	omege0.x	|- X = U. dom O
	omege0.a	|- ( ph -> A C_ X )
Assertion	omege0	|- ( ph -> 0 <_ ( O ` A ) )

Proof

Step	Hyp	Ref	Expression
1		omege0.o	|- ( ph -> O e. OutMeas )
2		omege0.x	|- X = U. dom O
3		omege0.a	|- ( ph -> A C_ X )
4		0xr	|- 0 e. RR*
5	4	a1i	|- ( ph -> 0 e. RR* )
6		pnfxr	|- +oo e. RR*
7	6	a1i	|- ( ph -> +oo e. RR* )
8	1 2 3	omecl	|- ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )
9		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ ( O ` A ) e. ( 0 [,] +oo ) ) -> 0 <_ ( O ` A ) )
10	5 7 8 9	syl3anc	|- ( ph -> 0 <_ ( O ` A ) )