Metamath Proof Explorer


Theorem supxrbnd1

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

Ref Expression
Assertion supxrbnd1 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 rexr x x *
3 ssel2 A * y A y *
4 xrlenlt x * y * x y ¬ y < x
5 2 3 4 syl2anr A * y A x x y ¬ y < x
6 5 an32s A * x y A x y ¬ y < x
7 6 rexbidva A * x y A x y y A ¬ y < x
8 rexnal y A ¬ y < x ¬ y A y < x
9 7 8 bitr2di A * x ¬ y A y < x y A x y
10 9 ralbidva A * x ¬ y A y < x x y A x y
11 1 10 bitr3id A * ¬ x y A y < x x y A x y
12 supxrunb1 A * x y A x y sup A * < = +∞
13 supxrcl A * sup A * < *
14 nltpnft sup A * < * sup A * < = +∞ ¬ sup A * < < +∞
15 13 14 syl A * sup A * < = +∞ ¬ sup A * < < +∞
16 11 12 15 3bitrd A * ¬ x y A y < x ¬ sup A * < < +∞
17 16 con4bid A * x y A y < x sup A * < < +∞