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 )