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 ) )