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* , < ) )