Metamath Proof Explorer

Theorem supxrre2

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

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

Proof

Step Hyp Ref Expression
1 supxrre1 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> sup ( A , RR* , < ) < +oo ) )
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 nltpnft 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
7 4 5 6 3syl 
 |-  ( A C_ RR -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
8 7 necon2abid 
 |-  ( A C_ RR -> ( sup ( A , RR* , < ) < +oo <-> sup ( A , RR* , < ) =/= +oo ) )
9 8 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) < +oo <-> sup ( A , RR* , < ) =/= +oo ) )
10 1 9 bitrd 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> sup ( A , RR* , < ) =/= +oo ) )