# 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 ) )`
` |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) < +oo <-> sup ( A , RR* , < ) =/= +oo ) )`
` |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> sup ( A , RR* , < ) =/= +oo ) )`