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

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