Theorem xrinf0

Description: The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 5-Sep-2020)

	Ref	Expression
Assertion	xrinf0	⊢ inf ( ∅ , ℝ* , < ) = +∞

Proof

Step	Hyp	Ref	Expression
1		xrltso	⊢ < Or ℝ*
2	1	a1i	⊢ ( ⊤ → < Or ℝ* )
3		pnfxr	⊢ +∞ ∈ ℝ*
4	3	a1i	⊢ ( ⊤ → +∞ ∈ ℝ* )
5		noel	⊢ ¬ 𝑦 ∈ ∅
6	5	pm2.21i	⊢ ( 𝑦 ∈ ∅ → ¬ 𝑦 < +∞ )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ∅ ) → ¬ 𝑦 < +∞ )
8		pnfnlt	⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ < 𝑦 )
9	8	pm2.21d	⊢ ( 𝑦 ∈ ℝ* → ( +∞ < 𝑦 → ∃ 𝑧 ∈ ∅ 𝑧 < 𝑦 ) )
10	9	imp	⊢ ( ( 𝑦 ∈ ℝ* ∧ +∞ < 𝑦 ) → ∃ 𝑧 ∈ ∅ 𝑧 < 𝑦 )
11	10	adantl	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ* ∧ +∞ < 𝑦 ) ) → ∃ 𝑧 ∈ ∅ 𝑧 < 𝑦 )
12	2 4 7 11	eqinfd	⊢ ( ⊤ → inf ( ∅ , ℝ* , < ) = +∞ )
13	12	mptru	⊢ inf ( ∅ , ℝ* , < ) = +∞