Metamath Proof Explorer

Theorem infxrpnf2

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

Ref Expression
Assertion infxrpnf2 
|- ( A C_ RR* -> inf ( ( A \ { +oo } ) , RR* , < ) = inf ( A , RR* , < ) )

Proof

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