Metamath Proof Explorer

Theorem supxrre1

Description: The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 supxrgtmnf 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> -oo < sup ( A , RR* , < ) )
2 ressxr 
 |-  RR C_ RR*
3 sstr 
 |-  ( ( A C_ RR /\ RR C_ RR* ) -> A C_ RR* )
4 2 3 mpan2 
 |-  ( A C_ RR -> A C_ RR* )
5 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
6 xrrebnd 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
7 4 5 6 3syl 
 |-  ( A C_ RR -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
8 7 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
9 1 8 mpbirand 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> sup ( A , RR* , < ) < +oo ) )