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