Theorem infxrbnd2

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

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

Proof

Step	Hyp	Ref	Expression
1		ralnex	|- ( A. x e. RR -. A. y e. A x <_ y <-> -. E. x e. RR A. y e. A x <_ y )
2		ssel2	|- ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
3		rexr	|- ( x e. RR -> x e. RR* )
4		simpl	|- ( ( y e. RR* /\ x e. RR* ) -> y e. RR* )
5		simpr	|- ( ( y e. RR* /\ x e. RR* ) -> x e. RR* )
6	4 5	xrltnled	|- ( ( y e. RR* /\ x e. RR* ) -> ( y < x <-> -. x <_ y ) )
7	2 3 6	syl2an	|- ( ( ( A C_ RR* /\ y e. A ) /\ x e. RR ) -> ( y < x <-> -. x <_ y ) )
8	7	an32s	|- ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( y < x <-> -. x <_ y ) )
9	8	rexbidva	|- ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A y < x <-> E. y e. A -. x <_ y ) )
10		rexnal	|- ( E. y e. A -. x <_ y <-> -. A. y e. A x <_ y )
11	9 10	bitr2di	|- ( ( A C_ RR* /\ x e. RR ) -> ( -. A. y e. A x <_ y <-> E. y e. A y < x ) )
12	11	ralbidva	|- ( A C_ RR* -> ( A. x e. RR -. A. y e. A x <_ y <-> A. x e. RR E. y e. A y < x ) )
13	1 12	bitr3id	|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A x <_ y <-> A. x e. RR E. y e. A y < x ) )
14		infxrunb2	|- ( A C_ RR* -> ( A. x e. RR E. y e. A y < x <-> inf ( A , RR* , < ) = -oo ) )
15		infxrcl	|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
16		ngtmnft	|- ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) = -oo <-> -. -oo < inf ( A , RR* , < ) ) )
17	15 16	syl	|- ( A C_ RR* -> ( inf ( A , RR* , < ) = -oo <-> -. -oo < inf ( A , RR* , < ) ) )
18	13 14 17	3bitrd	|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A x <_ y <-> -. -oo < inf ( A , RR* , < ) ) )
19	18	con4bid	|- ( A C_ RR* -> ( E. x e. RR A. y e. A x <_ y <-> -oo < inf ( A , RR* , < ) ) )