supxrmnf

Description: Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	supxrmnf	$⊢ A \subseteq ℝ^{} \to sup (A \cup \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		uncom	$⊢ A \cup \{−∞\} = \{−∞\} \cup A$
2	1	supeq1i	$⊢ sup (A \cup \{−∞\} ℝ^{} <) = sup (\{−∞\} \cup A ℝ^{} <)$
3		mnfxr	$⊢ −∞ \in ℝ^{*}$
4		snssi	$⊢ −∞ \in ℝ^{} \to \{−∞\} \subseteq ℝ^{}$
5	3 4	mp1i	$⊢ A \subseteq ℝ^{} \to \{−∞\} \subseteq ℝ^{}$
6		id	$⊢ A \subseteq ℝ^{} \to A \subseteq ℝ^{}$
7		xrltso	$⊢ < Or ℝ^{*}$
8		supsn	$⊢ (< Or ℝ^{} \land −∞ \in ℝ^{}) \to sup (\{−∞\} ℝ^{*} <) = −∞$
9	7 3 8	mp2an	$⊢ sup (\{−∞\} ℝ^{*} <) = −∞$
10		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
11		mnfle	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to −∞ \leq sup (A ℝ^{*} <)$
12	10 11	syl	$⊢ A \subseteq ℝ^{} \to −∞ \leq sup (A ℝ^{} <)$
13	9 12	eqbrtrid	$⊢ A \subseteq ℝ^{} \to sup (\{−∞\} ℝ^{} <) \leq sup (A ℝ^{*} <)$
14		supxrun	$⊢ (\{−∞\} \subseteq ℝ^{} \land A \subseteq ℝ^{} \land sup (\{−∞\} ℝ^{} <) \leq sup (A ℝ^{} <)) \to sup (\{−∞\} \cup A ℝ^{} <) = sup (A ℝ^{} <)$
15	5 6 13 14	syl3anc	$⊢ A \subseteq ℝ^{} \to sup (\{−∞\} \cup A ℝ^{} <) = sup (A ℝ^{*} <)$
16	2 15	eqtrid	$⊢ A \subseteq ℝ^{} \to sup (A \cup \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$

Metamath Proof Explorer