Theorem infxrlb

Description: A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infxrcl	|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
2	1	adantr	|- ( ( A C_ RR* /\ B e. A ) -> inf ( A , RR* , < ) e. RR* )
3		ssel2	|- ( ( A C_ RR* /\ B e. A ) -> B e. RR* )
4		xrltso	|- < Or RR*
5	4	a1i	|- ( A C_ RR* -> < Or RR* )
6		xrinfmss	|- ( A C_ RR* -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
7	5 6	inflb	|- ( A C_ RR* -> ( B e. A -> -. B < inf ( A , RR* , < ) ) )
8	7	imp	|- ( ( A C_ RR* /\ B e. A ) -> -. B < inf ( A , RR* , < ) )
9	2 3 8	xrnltled	|- ( ( A C_ RR* /\ B e. A ) -> inf ( A , RR* , < ) <_ B )