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