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* )
13 12 adantlr
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> y e. RR* )
14 rexr
 |-  ( x e. RR -> x e. RR* )
15 14 ad2antlr
 |-  ( ( ( 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 bitrdi
 |-  ( ( 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 bitrdi
 |-  ( 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 )
30 29 3adant2
 |-  ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> E. x e. RR A. y e. A y <_ x )
31 supxrre
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
32 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
33 31 32 eqeltrd
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) e. RR )
34 30 33 syld3an3
 |-  ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> sup ( A , RR* , < ) e. RR )