This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ⊆ ℝ* → sup ( ( 𝐴 ∪ { -∞ } ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( 𝐴 ∪ { -∞ } ) = ( { -∞ } ∪ 𝐴 )
2 1 supeq1i ⊢ sup ( ( 𝐴 ∪ { -∞ } ) , ℝ* , < ) = sup ( ( { -∞ } ∪ 𝐴 ) , ℝ* , < )
3 mnfxr ⊢ -∞ ∈ ℝ*
4 snssi ⊢ ( -∞ ∈ ℝ* → { -∞ } ⊆ ℝ* )
5 3 4 mp1i ⊢ ( 𝐴 ⊆ ℝ* → { -∞ } ⊆ ℝ* )
6 id ⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ⊆ ℝ* )
7 xrltso ⊢ < Or ℝ*
8 supsn ⊢ ( ( < Or ℝ* ∧ -∞ ∈ ℝ* ) → sup ( { -∞ } , ℝ* , < ) = -∞ )
9 7 3 8 mp2an ⊢ sup ( { -∞ } , ℝ* , < ) = -∞
10 supxrcl ⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
11 mnfle ⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → -∞ ≤ sup ( 𝐴 , ℝ* , < ) )
12 10 11 syl ⊢ ( 𝐴 ⊆ ℝ* → -∞ ≤ sup ( 𝐴 , ℝ* , < ) )
13 9 12 eqbrtrid ⊢ ( 𝐴 ⊆ ℝ* → sup ( { -∞ } , ℝ* , < ) ≤ sup ( 𝐴 , ℝ* , < ) )
14 supxrun ⊢ ( ( { -∞ } ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ∧ sup ( { -∞ } , ℝ* , < ) ≤ sup ( 𝐴 , ℝ* , < ) ) → sup ( ( { -∞ } ∪ 𝐴 ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )
15 5 6 13 14 syl3anc ⊢ ( 𝐴 ⊆ ℝ* → sup ( ( { -∞ } ∪ 𝐴 ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )
16 2 15 eqtrid ⊢ ( 𝐴 ⊆ ℝ* → sup ( ( 𝐴 ∪ { -∞ } ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )