Metamath Proof Explorer


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