Metamath Proof Explorer


Theorem suprnub

Description: An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion suprnub A A x y A y x B ¬ B < sup A < z A ¬ B < z

Proof

Step Hyp Ref Expression
1 suprlub A A x y A y x B B < sup A < z A B < z
2 1 notbid A A x y A y x B ¬ B < sup A < ¬ z A B < z
3 ralnex z A ¬ B < z ¬ z A B < z
4 2 3 bitr4di A A x y A y x B ¬ B < sup A < z A ¬ B < z