Theorem 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 ( ∅ , ℝ* , < ) = -∞

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ℝ*
2		mnfxr	⊢ -∞ ∈ ℝ*
3		ral0	⊢ ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦
4		rexr	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
5		nltmnf	⊢ ( 𝑦 ∈ ℝ* → ¬ 𝑦 < -∞ )
6	4 5	syl	⊢ ( 𝑦 ∈ ℝ → ¬ 𝑦 < -∞ )
7	6	pm2.21d	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) )
8	7	rgen	⊢ ∀ 𝑦 ∈ ℝ ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 )
9		supxr	⊢ ( ( ( ∅ ⊆ ℝ* ∧ -∞ ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ) → sup ( ∅ , ℝ* , < ) = -∞ )
10	1 2 3 8 9	mp4an	⊢ sup ( ∅ , ℝ* , < ) = -∞