Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

	Ref	Expression
Assertion	infxrgelb	|- ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> A. x e. A B <_ x ) )

Proof

Step	Hyp	Ref	Expression
1		xrltso	|- < Or RR*
2	1	a1i	|- ( A C_ RR* -> < Or RR* )
3		xrinfmss	|- ( A C_ RR* -> E. z e. RR* ( A. y e. A -. y < z /\ A. y e. RR* ( z < y -> E. x e. A x < y ) ) )
4		id	|- ( A C_ RR* -> A C_ RR* )
5	2 3 4	infglbb	|- ( ( A C_ RR* /\ B e. RR* ) -> ( inf ( A , RR* , < ) < B <-> E. x e. A x < B ) )
6	5	notbid	|- ( ( A C_ RR* /\ B e. RR* ) -> ( -. inf ( A , RR* , < ) < B <-> -. E. x e. A x < B ) )
7		ralnex	|- ( A. x e. A -. x < B <-> -. E. x e. A x < B )
8	6 7	bitr4di	|- ( ( A C_ RR* /\ B e. RR* ) -> ( -. inf ( A , RR* , < ) < B <-> A. x e. A -. x < B ) )
9		id	|- ( B e. RR* -> B e. RR* )
10		infxrcl	|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
11		xrlenlt	|- ( ( B e. RR* /\ inf ( A , RR* , < ) e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> -. inf ( A , RR* , < ) < B ) )
12	9 10 11	syl2anr	|- ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> -. inf ( A , RR* , < ) < B ) )
13		simplr	|- ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> B e. RR* )
14		simpl	|- ( ( A C_ RR* /\ B e. RR* ) -> A C_ RR* )
15	14	sselda	|- ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> x e. RR* )
16	13 15	xrlenltd	|- ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> ( B <_ x <-> -. x < B ) )
17	16	ralbidva	|- ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. A B <_ x <-> A. x e. A -. x < B ) )
18	8 12 17	3bitr4d	|- ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> A. x e. A B <_ x ) )