Metamath Proof Explorer


Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrgelb A * B * B sup A * < x A B x

Proof

Step Hyp Ref Expression
1 xrltso < Or *
2 1 a1i A * < Or *
3 xrinfmss A * z * y A ¬ y < z y * z < y x A x < y
4 id A * A *
5 2 3 4 infglbb A * B * sup A * < < B x A x < B
6 5 notbid A * B * ¬ sup A * < < B ¬ x A x < B
7 ralnex x A ¬ x < B ¬ x A x < B
8 6 7 bitr4di A * B * ¬ sup A * < < B x A ¬ x < B
9 id B * B *
10 infxrcl A * sup A * < *
11 xrlenlt B * sup A * < * B sup A * < ¬ sup A * < < B
12 9 10 11 syl2anr A * B * B sup A * < ¬ sup A * < < B
13 simplr A * B * x A B *
14 simpl A * B * A *
15 14 sselda A * B * x A x *
16 13 15 xrlenltd A * B * x A B x ¬ x < B
17 16 ralbidva A * B * x A B x x A ¬ x < B
18 8 12 17 3bitr4d A * B * B sup A * < x A B x