Metamath Proof Explorer

Theorem supxrmnf2

Description: Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion supxrmnf2 
|- ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ssdifss 
 |-  ( A C_ RR* -> ( A \ { -oo } ) C_ RR* )
2 supxrmnf 
 |-  ( ( A \ { -oo } ) C_ RR* -> sup ( ( ( A \ { -oo } ) u. { -oo } ) , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
3 1 2 syl 
 |-  ( A C_ RR* -> sup ( ( ( A \ { -oo } ) u. { -oo } ) , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
4 3 adantr 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> sup ( ( ( A \ { -oo } ) u. { -oo } ) , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
5 difsnid 
 |-  ( -oo e. A -> ( ( A \ { -oo } ) u. { -oo } ) = A )
6 5 supeq1d 
 |-  ( -oo e. A -> sup ( ( ( A \ { -oo } ) u. { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
7 6 adantl 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> sup ( ( ( A \ { -oo } ) u. { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
8 4 7 eqtr3d 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
9 difsn 
 |-  ( -. -oo e. A -> ( A \ { -oo } ) = A )
10 9 supeq1d 
 |-  ( -. -oo e. A -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
11 10 adantl 
 |-  ( ( A C_ RR* /\ -. -oo e. A ) -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
12 8 11 pm2.61dan 
 |-  ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )