supxrmnf2

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

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

Step	Hyp	Ref	Expression
1		ssdifss	$⊢ A \subseteq ℝ^{} \to A ∖ \{−∞\} \subseteq ℝ^{}$
2		supxrmnf	$⊢ A ∖ \{−∞\} \subseteq ℝ^{} \to sup ((A ∖ \{−∞\}) \cup \{−∞\} ℝ^{} <) = sup (A ∖ \{−∞\} ℝ^{*} <)$
3	1 2	syl	$⊢ A \subseteq ℝ^{} \to sup ((A ∖ \{−∞\}) \cup \{−∞\} ℝ^{} <) = sup (A ∖ \{−∞\} ℝ^{*} <)$
4	3	adantr	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to sup ((A ∖ \{−∞\}) \cup \{−∞\} ℝ^{} <) = sup (A ∖ \{−∞\} ℝ^{*} <)$
5		difsnid	$⊢ −∞ \in A \to (A ∖ \{−∞\}) \cup \{−∞\} = A$
6	5	supeq1d	$⊢ −∞ \in A \to sup ((A ∖ \{−∞\}) \cup \{−∞\} ℝ^{} <) = sup (A ℝ^{} <)$
7	6	adantl	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to sup ((A ∖ \{−∞\}) \cup \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$
8	4 7	eqtr3d	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$
9		difsn	$⊢ \neg −∞ \in A \to A ∖ \{−∞\} = A$
10	9	supeq1d	$⊢ \neg −∞ \in A \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{} <)$
11	10	adantl	$⊢ (A \subseteq ℝ^{} \land \neg −∞ \in A) \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$
12	8 11	pm2.61dan	$⊢ A \subseteq ℝ^{} \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$

Metamath Proof Explorer