Metamath Proof Explorer


Theorem suprleub

Description: The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion suprleub A A x y A y x B sup A < B z A z B

Proof

Step Hyp Ref Expression
1 suprnub A A x y A y x B ¬ B < sup A < w A ¬ B < w
2 suprcl A A x y A y x sup A <
3 lenlt sup A < B sup A < B ¬ B < sup A <
4 2 3 sylan A A x y A y x B sup A < B ¬ B < sup A <
5 simpl1 A A x y A y x B A
6 5 sselda A A x y A y x B w A w
7 simplr A A x y A y x B w A B
8 6 7 lenltd A A x y A y x B w A w B ¬ B < w
9 8 ralbidva A A x y A y x B w A w B w A ¬ B < w
10 1 4 9 3bitr4d A A x y A y x B sup A < B w A w B
11 breq1 w = z w B z B
12 11 cbvralvw w A w B z A z B
13 10 12 bitrdi A A x y A y x B sup A < B z A z B