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

Metamath Proof Explorer

Theorem infxrunb2

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion infxrunb2 
|- ( A C_ RR* -> ( A. x e. RR E. y e. A y < x <-> inf ( A , RR* , < ) = -oo ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x A C_ RR*
2 nfra1 
 |-  F/ x A. x e. RR E. y e. A y < x
3 1 2 nfan 
 |-  F/ x ( A C_ RR* /\ A. x e. RR E. y e. A y < x )
4 nfv 
 |-  F/ y A C_ RR*
5 nfcv 
 |-  F/_ y RR
6 nfre1 
 |-  F/ y E. y e. A y < x
7 5 6 nfralw 
 |-  F/ y A. x e. RR E. y e. A y < x
8 4 7 nfan 
 |-  F/ y ( A C_ RR* /\ A. x e. RR E. y e. A y < x )
9 simpl 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y < x ) -> A C_ RR* )
10 mnfxr 
 |-  -oo e. RR*
11 10 a1i 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y < x ) -> -oo e. RR* )
12 ssel2 
 |-  ( ( A C_ RR* /\ x e. A ) -> x e. RR* )
13 nltmnf 
 |-  ( x e. RR* -> -. x < -oo )
14 12 13 syl 
 |-  ( ( A C_ RR* /\ x e. A ) -> -. x < -oo )
15 14 ralrimiva 
 |-  ( A C_ RR* -> A. x e. A -. x < -oo )
16 15 adantr 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y < x ) -> A. x e. A -. x < -oo )
17 ralimralim 
 |-  ( A. x e. RR E. y e. A y < x -> A. x e. RR ( -oo < x -> E. y e. A y < x ) )
18 17 adantl 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y < x ) -> A. x e. RR ( -oo < x -> E. y e. A y < x ) )
19 3 8 9 11 16 18 infxr 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y < x ) -> inf ( A , RR* , < ) = -oo )
20 19 ex 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A y < x -> inf ( A , RR* , < ) = -oo ) )
21 rexr 
 |-  ( x e. RR -> x e. RR* )
22 21 adantl 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> x e. RR* )
23 simpl 
 |-  ( ( inf ( A , RR* , < ) = -oo /\ x e. RR ) -> inf ( A , RR* , < ) = -oo )
24 mnflt 
 |-  ( x e. RR -> -oo < x )
25 24 adantl 
 |-  ( ( inf ( A , RR* , < ) = -oo /\ x e. RR ) -> -oo < x )
26 23 25 eqbrtrd 
 |-  ( ( inf ( A , RR* , < ) = -oo /\ x e. RR ) -> inf ( A , RR* , < ) < x )
27 26 adantll 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> inf ( A , RR* , < ) < x )
28 xrltso 
 |-  < Or RR*
29 28 a1i 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> < Or RR* )
30 xrinfmss 
 |-  ( A C_ RR* -> E. z e. RR* ( A. w e. A -. w < z /\ A. w e. RR* ( z < w -> E. y e. A y < w ) ) )
31 30 ad2antrr 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> E. z e. RR* ( A. w e. A -. w < z /\ A. w e. RR* ( z < w -> E. y e. A y < w ) ) )
32 29 31 infglb 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> ( ( x e. RR* /\ inf ( A , RR* , < ) < x ) -> E. y e. A y < x ) )
33 22 27 32 mp2and 
 |-  ( ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) /\ x e. RR ) -> E. y e. A y < x )
34 33 ralrimiva 
 |-  ( ( A C_ RR* /\ inf ( A , RR* , < ) = -oo ) -> A. x e. RR E. y e. A y < x )
35 34 ex 
 |-  ( A C_ RR* -> ( inf ( A , RR* , < ) = -oo -> A. x e. RR E. y e. A y < x ) )
36 20 35 impbid 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A y < x <-> inf ( A , RR* , < ) = -oo ) )