Theorem infxrge0lb

Description: A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	infxrge0lb.a	|- ( ph -> A C_ ( 0 [,] +oo ) )
	infxrge0lb.b	|- ( ph -> B e. A )
Assertion	infxrge0lb	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) <_ B )

Proof

Step	Hyp	Ref	Expression
1		infxrge0lb.a	|- ( ph -> A C_ ( 0 [,] +oo ) )
2		infxrge0lb.b	|- ( ph -> B e. A )
3		iccssxr	|- ( 0 [,] +oo ) C_ RR*
4		xrltso	|- < Or RR*
5		soss	|- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
6	3 4 5	mp2	|- < Or ( 0 [,] +oo )
7	6	a1i	|- ( ph -> < Or ( 0 [,] +oo ) )
8		xrge0infss	|- ( A C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. A z < y ) ) )
9	1 8	syl	|- ( ph -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. A z < y ) ) )
10	7 9	infcl	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
11	3 10	sselid	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. RR* )
12	1 2	sseldd	|- ( ph -> B e. ( 0 [,] +oo ) )
13	3 12	sselid	|- ( ph -> B e. RR* )
14	7 9	inflb	|- ( ph -> ( B e. A -> -. B < inf ( A , ( 0 [,] +oo ) , < ) ) )
15	2 14	mpd	|- ( ph -> -. B < inf ( A , ( 0 [,] +oo ) , < ) )
16	11 13 15	xrnltled	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) <_ B )