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\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$$

Proof

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