Metamath Proof Explorer


Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 supxrlub A * B * B < sup A * < x A B < x
2 1 notbid A * B * ¬ B < sup A * < ¬ x A B < x
3 ralnex x A ¬ B < x ¬ x A B < x
4 2 3 bitr4di A * B * ¬ B < sup A * < x A ¬ B < x
5 supxrcl A * sup A * < *
6 xrlenlt sup A * < * B * sup A * < B ¬ B < sup A * <
7 5 6 sylan A * B * sup A * < B ¬ B < sup A * <
8 simpl A * B * A *
9 8 sselda A * B * x A x *
10 simplr A * B * x A B *
11 9 10 xrlenltd A * B * x A x B ¬ B < x
12 11 ralbidva A * B * x A x B x A ¬ B < x
13 4 7 12 3bitr4d A * B * sup A * < B x A x B