xrsup0

Description: The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005)

		Ref	Expression
	Assertion	xrsup0	$⊢ sup (\emptyset ℝ^{*} <) = −∞$

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq ℝ^{*}$
2		mnfxr	$⊢ −∞ \in ℝ^{*}$
3		ral0	$⊢ \forall y \in \emptyset \neg −∞ < y$
4		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
5		nltmnf	$⊢ y \in ℝ^{*} \to \neg y < −∞$
6	4 5	syl	$⊢ y \in ℝ \to \neg y < −∞$
7	6	pm2.21d	$⊢ y \in ℝ \to (y < −∞ \to \exists z \in \emptyset y < z)$
8	7	rgen	$⊢ \forall y \in ℝ (y < −∞ \to \exists z \in \emptyset y < z)$
9		supxr	$⊢ ((\emptyset \subseteq ℝ^{} \land −∞ \in ℝ^{}) \land (\forall y \in \emptyset \neg −∞ < y \land \forall y \in ℝ (y < −∞ \to \exists z \in \emptyset y < z))) \to sup (\emptyset ℝ^{*} <) = −∞$
10	1 2 3 8 9	mp4an	$⊢ sup (\emptyset ℝ^{*} <) = −∞$

Metamath Proof Explorer