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 ) )