Theorem infxrge0gelb

Description: The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infxrge0glb.a	|- ( ph -> A C_ ( 0 [,] +oo ) )
2		infxrge0glb.b	|- ( ph -> B e. ( 0 [,] +oo ) )
3	1 2	infxrge0glb	|- ( ph -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. x e. A x < B ) )
4	3	notbid	|- ( ph -> ( -. inf ( A , ( 0 [,] +oo ) , < ) < B <-> -. E. x e. A x < B ) )
5		iccssxr	|- ( 0 [,] +oo ) C_ RR*
6	5 2	sselid	|- ( ph -> B e. RR* )
7		xrltso	|- < Or RR*
8		soss	|- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
9	5 7 8	mp2	|- < Or ( 0 [,] +oo )
10	9	a1i	|- ( ph -> < Or ( 0 [,] +oo ) )
11		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 ) ) )
12	1 11	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 ) ) )
13	10 12	infcl	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
14	5 13	sselid	|- ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. RR* )
15	6 14	xrlenltd	|- ( ph -> ( B <_ inf ( A , ( 0 [,] +oo ) , < ) <-> -. inf ( A , ( 0 [,] +oo ) , < ) < B ) )
16	6	adantr	|- ( ( ph /\ x e. A ) -> B e. RR* )
17	1 5	sstrdi	|- ( ph -> A C_ RR* )
18	17	sselda	|- ( ( ph /\ x e. A ) -> x e. RR* )
19	16 18	xrlenltd	|- ( ( ph /\ x e. A ) -> ( B <_ x <-> -. x < B ) )
20	19	ralbidva	|- ( ph -> ( A. x e. A B <_ x <-> A. x e. A -. x < B ) )
21		ralnex	|- ( A. x e. A -. x < B <-> -. E. x e. A x < B )
22	20 21	bitrdi	|- ( ph -> ( A. x e. A B <_ x <-> -. E. x e. A x < B ) )
23	4 15 22	3bitr4d	|- ( ph -> ( B <_ inf ( A , ( 0 [,] +oo ) , < ) <-> A. x e. A B <_ x ) )