Metamath Proof Explorer


Theorem supxrbnd2

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

Ref Expression
Assertion supxrbnd2 A * x y A y x sup A * < < +∞

Proof

Step Hyp Ref Expression
1 ralnex x ¬ y A y x ¬ x y A y x
2 ssel2 A * y A y *
3 rexr x x *
4 xrlenlt y * x * y x ¬ x < y
5 4 con2bid y * x * x < y ¬ y x
6 2 3 5 syl2an A * y A x x < y ¬ y x
7 6 an32s A * x y A x < y ¬ y x
8 7 rexbidva A * x y A x < y y A ¬ y x
9 rexnal y A ¬ y x ¬ y A y x
10 8 9 bitr2di A * x ¬ y A y x y A x < y
11 10 ralbidva A * x ¬ y A y x x y A x < y
12 1 11 bitr3id A * ¬ x y A y x x y A x < y
13 supxrunb2 A * x y A x < y sup A * < = +∞
14 supxrcl A * sup A * < *
15 nltpnft sup A * < * sup A * < = +∞ ¬ sup A * < < +∞
16 14 15 syl A * sup A * < = +∞ ¬ sup A * < < +∞
17 12 13 16 3bitrd A * ¬ x y A y x ¬ sup A * < < +∞
18 17 con4bid A * x y A y x sup A * < < +∞