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 ( (/) , RR* , < ) = +oo

Proof

Step	Hyp	Ref	Expression
1		xrltso	|- < Or RR*
2	1	a1i	|- ( T. -> < Or RR* )
3		pnfxr	|- +oo e. RR*
4	3	a1i	|- ( T. -> +oo e. RR* )
5		noel	|- -. y e. (/)
6	5	pm2.21i	|- ( y e. (/) -> -. y < +oo )
7	6	adantl	|- ( ( T. /\ y e. (/) ) -> -. y < +oo )
8		pnfnlt	|- ( y e. RR* -> -. +oo < y )
9	8	pm2.21d	|- ( y e. RR* -> ( +oo < y -> E. z e. (/) z < y ) )
10	9	imp	|- ( ( y e. RR* /\ +oo < y ) -> E. z e. (/) z < y )
11	10	adantl	|- ( ( T. /\ ( y e. RR* /\ +oo < y ) ) -> E. z e. (/) z < y )
12	2 4 7 11	eqinfd	|- ( T. -> inf ( (/) , RR* , < ) = +oo )
13	12	mptru	|- inf ( (/) , RR* , < ) = +oo