Metamath Proof Explorer


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*BAsupA*<B

Proof

Step Hyp Ref Expression
1 infxrcl A*supA*<*
2 1 adantr A*BAsupA*<*
3 ssel2 A*BAB*
4 xrltso <Or*
5 4 a1i A*<Or*
6 xrinfmss A*x*yA¬y<xy*x<yzAz<y
7 5 6 inflb A*BA¬B<supA*<
8 7 imp A*BA¬B<supA*<
9 2 3 8 xrnltled A*BAsupA*<B