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