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 ( (/) , 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