Metamath Proof Explorer


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