This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (\emptyset ℝ^{*} <) = +∞$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$⊢ < Or ℝ^{*}$
2	1	a1i	$⊢ ⊤ \to < Or ℝ^{*}$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4	3	a1i	$⊢ ⊤ \to +∞ \in ℝ^{*}$
5		noel	$⊢ \neg y \in \emptyset$
6	5	pm2.21i	$⊢ y \in \emptyset \to \neg y < +∞$
7	6	adantl	$⊢ (⊤ \land y \in \emptyset) \to \neg y < +∞$
8		pnfnlt	$⊢ y \in ℝ^{*} \to \neg +∞ < y$
9	8	pm2.21d	$⊢ y \in ℝ^{*} \to (+∞ < y \to \exists z \in \emptyset z < y)$
10	9	imp	$⊢ (y \in ℝ^{*} \land +∞ < y) \to \exists z \in \emptyset z < y$
11	10	adantl	$⊢ (⊤ \land (y \in ℝ^{*} \land +∞ < y)) \to \exists z \in \emptyset z < y$
12	2 4 7 11	eqinfd	$⊢ ⊤ \to inf (\emptyset ℝ^{*} <) = +∞$
13	12	mptru	$⊢ inf (\emptyset ℝ^{*} <) = +∞$