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

Metamath Proof Explorer

Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrgelb 
|- ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> A. x e. A B <_ x ) )

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 1 a1i 
 |-  ( A C_ RR* -> < Or RR* )
3 xrinfmss 
 |-  ( A C_ RR* -> E. z e. RR* ( A. y e. A -. y < z /\ A. y e. RR* ( z < y -> E. x e. A x < y ) ) )
4 id 
 |-  ( A C_ RR* -> A C_ RR* )
5 2 3 4 infglbb 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( inf ( A , RR* , < ) < B <-> E. x e. A x < B ) )
6 5 notbid 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( -. inf ( A , RR* , < ) < B <-> -. E. x e. A x < B ) )
7 ralnex 
 |-  ( A. x e. A -. x < B <-> -. E. x e. A x < B )
8 6 7 bitr4di 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( -. inf ( A , RR* , < ) < B <-> A. x e. A -. x < B ) )
9 id 
 |-  ( B e. RR* -> B e. RR* )
10 infxrcl 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
11 xrlenlt 
 |-  ( ( B e. RR* /\ inf ( A , RR* , < ) e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> -. inf ( A , RR* , < ) < B ) )
12 9 10 11 syl2anr 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> -. inf ( A , RR* , < ) < B ) )
13 simplr 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> B e. RR* )
14 simpl 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> A C_ RR* )
15 14 sselda 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> x e. RR* )
16 13 15 xrlenltd 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ x e. A ) -> ( B <_ x <-> -. x < B ) )
17 16 ralbidva 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. A B <_ x <-> A. x e. A -. x < B ) )
18 8 12 17 3bitr4d 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( B <_ inf ( A , RR* , < ) <-> A. x e. A B <_ x ) )