Theorem infxrglb

Description: The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

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 ) )