# Metamath Proof Explorer

## Theorem supxrbnd

Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrbnd
`|- ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> sup ( A , RR* , < ) e. RR )`

### Proof

Step Hyp Ref Expression
1 ressxr
` |-  RR C_ RR*`
2 sstr
` |-  ( ( A C_ RR /\ RR C_ RR* ) -> A C_ RR* )`
3 1 2 mpan2
` |-  ( A C_ RR -> A C_ RR* )`
4 supxrcl
` |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )`
5 pnfxr
` |-  +oo e. RR*`
6 xrltne
` |-  ( ( sup ( A , RR* , < ) e. RR* /\ +oo e. RR* /\ sup ( A , RR* , < ) < +oo ) -> +oo =/= sup ( A , RR* , < ) )`
7 5 6 mp3an2
` |-  ( ( sup ( A , RR* , < ) e. RR* /\ sup ( A , RR* , < ) < +oo ) -> +oo =/= sup ( A , RR* , < ) )`
8 7 necomd
` |-  ( ( sup ( A , RR* , < ) e. RR* /\ sup ( A , RR* , < ) < +oo ) -> sup ( A , RR* , < ) =/= +oo )`
9 8 ex
` |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) < +oo -> sup ( A , RR* , < ) =/= +oo ) )`
10 4 9 syl
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) < +oo -> sup ( A , RR* , < ) =/= +oo ) )`
11 supxrunb2
` |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y <-> sup ( A , RR* , < ) = +oo ) )`
12 ssel2
` |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> y e. RR* )`
14 rexr
` |-  ( x e. RR -> x e. RR* )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> x e. RR* )`
16 xrlenlt
` |-  ( ( y e. RR* /\ x e. RR* ) -> ( y <_ x <-> -. x < y ) )`
17 16 con2bid
` |-  ( ( y e. RR* /\ x e. RR* ) -> ( x < y <-> -. y <_ x ) )`
18 13 15 17 syl2anc
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( x < y <-> -. y <_ x ) )`
19 18 rexbidva
` |-  ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A x < y <-> E. y e. A -. y <_ x ) )`
20 rexnal
` |-  ( E. y e. A -. y <_ x <-> -. A. y e. A y <_ x )`
21 19 20 syl6bb
` |-  ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A x < y <-> -. A. y e. A y <_ x ) )`
22 21 ralbidva
` |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y <-> A. x e. RR -. A. y e. A y <_ x ) )`
23 11 22 bitr3d
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo <-> A. x e. RR -. A. y e. A y <_ x ) )`
24 ralnex
` |-  ( A. x e. RR -. A. y e. A y <_ x <-> -. E. x e. RR A. y e. A y <_ x )`
25 23 24 syl6bb
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo <-> -. E. x e. RR A. y e. A y <_ x ) )`
26 25 necon2abid
` |-  ( A C_ RR* -> ( E. x e. RR A. y e. A y <_ x <-> sup ( A , RR* , < ) =/= +oo ) )`
27 10 26 sylibrd
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) < +oo -> E. x e. RR A. y e. A y <_ x ) )`
28 27 imp
` |-  ( ( A C_ RR* /\ sup ( A , RR* , < ) < +oo ) -> E. x e. RR A. y e. A y <_ x )`
29 3 28 sylan
` |-  ( ( A C_ RR /\ sup ( A , RR* , < ) < +oo ) -> E. x e. RR A. y e. A y <_ x )`
` |-  ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> E. x e. RR A. y e. A y <_ x )`
` |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )`
` |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )`
` |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) e. RR )`
` |-  ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> sup ( A , RR* , < ) e. RR )`