Metamath Proof Explorer

Theorem supxrgtmnf

Description: The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006)

Ref Expression
Assertion supxrgtmnf 
|- ( ( A C_ RR /\ A =/= (/) ) -> -oo < sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supxrbnd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ sup ( A , RR* , < ) < +oo ) -> sup ( A , RR* , < ) e. RR )
2 1 3expia 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) < +oo -> sup ( A , RR* , < ) e. RR ) )
3 2 con3d 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( -. sup ( A , RR* , < ) e. RR -> -. sup ( A , RR* , < ) < +oo ) )
4 ressxr 
 |-  RR C_ RR*
5 sstr 
 |-  ( ( A C_ RR /\ RR C_ RR* ) -> A C_ RR* )
6 4 5 mpan2 
 |-  ( A C_ RR -> A C_ RR* )
7 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
8 6 7 syl 
 |-  ( A C_ RR -> sup ( A , RR* , < ) e. RR* )
9 8 adantr 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> sup ( A , RR* , < ) e. RR* )
10 nltpnft 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
11 9 10 syl 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
12 3 11 sylibrd 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( -. sup ( A , RR* , < ) e. RR -> sup ( A , RR* , < ) = +oo ) )
13 12 orrd 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR \/ sup ( A , RR* , < ) = +oo ) )
14 mnfltxr 
 |-  ( ( sup ( A , RR* , < ) e. RR \/ sup ( A , RR* , < ) = +oo ) -> -oo < sup ( A , RR* , < ) )
15 13 14 syl 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> -oo < sup ( A , RR* , < ) )