Metamath Proof Explorer

Theorem supxrmnf

Description: Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrmnf 
|- ( A C_ RR* -> sup ( ( A u. { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( A u. { -oo } ) = ( { -oo } u. A )
2 1 supeq1i 
 |-  sup ( ( A u. { -oo } ) , RR* , < ) = sup ( ( { -oo } u. A ) , RR* , < )
3 mnfxr 
 |-  -oo e. RR*
4 snssi 
 |-  ( -oo e. RR* -> { -oo } C_ RR* )
5 3 4 mp1i 
 |-  ( A C_ RR* -> { -oo } C_ RR* )
6 id 
 |-  ( A C_ RR* -> A C_ RR* )
7 xrltso 
 |-  < Or RR*
8 supsn 
 |-  ( ( < Or RR* /\ -oo e. RR* ) -> sup ( { -oo } , RR* , < ) = -oo )
9 7 3 8 mp2an 
 |-  sup ( { -oo } , RR* , < ) = -oo
10 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
11 mnfle 
 |-  ( sup ( A , RR* , < ) e. RR* -> -oo <_ sup ( A , RR* , < ) )
12 10 11 syl 
 |-  ( A C_ RR* -> -oo <_ sup ( A , RR* , < ) )
13 9 12 eqbrtrid 
 |-  ( A C_ RR* -> sup ( { -oo } , RR* , < ) <_ sup ( A , RR* , < ) )
14 supxrun 
 |-  ( ( { -oo } C_ RR* /\ A C_ RR* /\ sup ( { -oo } , RR* , < ) <_ sup ( A , RR* , < ) ) -> sup ( ( { -oo } u. A ) , RR* , < ) = sup ( A , RR* , < ) )
15 5 6 13 14 syl3anc 
 |-  ( A C_ RR* -> sup ( ( { -oo } u. A ) , RR* , < ) = sup ( A , RR* , < ) )
16 2 15 eqtrid 
 |-  ( A C_ RR* -> sup ( ( A u. { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )