Metamath Proof Explorer


Theorem suprub

Description: A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004)

Ref Expression
Assertion suprub A A x y A y x B A B sup A <

Proof

Step Hyp Ref Expression
1 simp1 A A x y A y x A
2 1 sselda A A x y A y x B A B
3 suprcl A A x y A y x sup A <
4 3 adantr A A x y A y x B A sup A <
5 ltso < Or
6 5 a1i A A x y A y x < Or
7 sup3 A A x y A y x x y A ¬ x < y y y < x z A y < z
8 6 7 supub A A x y A y x B A ¬ sup A < < B
9 8 imp A A x y A y x B A ¬ sup A < < B
10 2 4 9 nltled A A x y A y x B A B sup A <