Metamath Proof Explorer

Theorem supxrre3

Description: The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion supxrre3 
|- ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> E. x e. RR A. y e. A y <_ x ) )

Proof

Step Hyp Ref Expression
1 supxrre1 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> sup ( A , RR* , < ) < +oo ) )
2 id 
 |-  ( A C_ RR -> A C_ RR )
3 rexr 
 |-  ( x e. RR -> x e. RR* )
4 3 ssriv 
 |-  RR C_ RR*
5 4 a1i 
 |-  ( A C_ RR -> RR C_ RR* )
6 2 5 sstrd 
 |-  ( A C_ RR -> A C_ RR* )
7 supxrbnd2 
 |-  ( A C_ RR* -> ( E. x e. RR A. y e. A y <_ x <-> sup ( A , RR* , < ) < +oo ) )
8 6 7 syl 
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A y <_ x <-> sup ( A , RR* , < ) < +oo ) )
9 8 bicomd 
 |-  ( A C_ RR -> ( sup ( A , RR* , < ) < +oo <-> E. x e. RR A. y e. A y <_ x ) )
10 9 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) < +oo <-> E. x e. RR A. y e. A y <_ x ) )
11 1 10 bitrd 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> E. x e. RR A. y e. A y <_ x ) )