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

Metamath Proof Explorer

Theorem infmremnf

Description: The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion infmremnf 
|- inf ( RR , RR* , < ) = -oo

Proof

Step Hyp Ref Expression
1 reltxrnmnf 
 |-  A. x e. RR* ( -oo < x -> E. z e. RR z < x )
2 xrltso 
 |-  < Or RR*
3 2 a1i 
 |-  ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> < Or RR* )
4 mnfxr 
 |-  -oo e. RR*
5 4 a1i 
 |-  ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> -oo e. RR* )
6 rexr 
 |-  ( y e. RR -> y e. RR* )
7 nltmnf 
 |-  ( y e. RR* -> -. y < -oo )
8 6 7 syl 
 |-  ( y e. RR -> -. y < -oo )
9 8 adantl 
 |-  ( ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) /\ y e. RR ) -> -. y < -oo )
10 breq2 
 |-  ( x = y -> ( -oo < x <-> -oo < y ) )
11 breq2 
 |-  ( x = y -> ( z < x <-> z < y ) )
12 11 rexbidv 
 |-  ( x = y -> ( E. z e. RR z < x <-> E. z e. RR z < y ) )
13 10 12 imbi12d 
 |-  ( x = y -> ( ( -oo < x -> E. z e. RR z < x ) <-> ( -oo < y -> E. z e. RR z < y ) ) )
14 13 rspcv 
 |-  ( y e. RR* -> ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> ( -oo < y -> E. z e. RR z < y ) ) )
15 14 com23 
 |-  ( y e. RR* -> ( -oo < y -> ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> E. z e. RR z < y ) ) )
16 15 imp 
 |-  ( ( y e. RR* /\ -oo < y ) -> ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> E. z e. RR z < y ) )
17 16 impcom 
 |-  ( ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) /\ ( y e. RR* /\ -oo < y ) ) -> E. z e. RR z < y )
18 3 5 9 17 eqinfd 
 |-  ( A. x e. RR* ( -oo < x -> E. z e. RR z < x ) -> inf ( RR , RR* , < ) = -oo )
19 1 18 ax-mp 
 |-  inf ( RR , RR* , < ) = -oo