Metamath Proof Explorer

Theorem infregelb

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013) (Revised by AV, 4-Sep-2020) (Proof modification is discouraged.)

Ref Expression
Assertion infregelb 
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B <_ inf ( A , RR , < ) <-> A. z e. A B <_ z ) )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 1 a1i 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> < Or RR )
3 infm3 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. w e. A w < y ) ) )
4 simp1 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> A C_ RR )
5 2 3 4 infglbb 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( inf ( A , RR , < ) < B <-> E. w e. A w < B ) )
6 5 notbid 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( -. inf ( A , RR , < ) < B <-> -. E. w e. A w < B ) )
7 infrecl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) e. RR )
8 7 anim1i 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( inf ( A , RR , < ) e. RR /\ B e. RR ) )
9 8 ancomd 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B e. RR /\ inf ( A , RR , < ) e. RR ) )
10 lenlt 
 |-  ( ( B e. RR /\ inf ( A , RR , < ) e. RR ) -> ( B <_ inf ( A , RR , < ) <-> -. inf ( A , RR , < ) < B ) )
11 9 10 syl 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B <_ inf ( A , RR , < ) <-> -. inf ( A , RR , < ) < B ) )
12 simplr 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ w e. A ) -> B e. RR )
13 ssel 
 |-  ( A C_ RR -> ( w e. A -> w e. RR ) )
14 13 adantr 
 |-  ( ( A C_ RR /\ B e. RR ) -> ( w e. A -> w e. RR ) )
15 14 imp 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ w e. A ) -> w e. RR )
16 12 15 lenltd 
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ w e. A ) -> ( B <_ w <-> -. w < B ) )
17 16 ralbidva 
 |-  ( ( A C_ RR /\ B e. RR ) -> ( A. w e. A B <_ w <-> A. w e. A -. w < B ) )
18 17 3ad2antl1 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( A. w e. A B <_ w <-> A. w e. A -. w < B ) )
19 ralnex 
 |-  ( A. w e. A -. w < B <-> -. E. w e. A w < B )
20 18 19 bitrdi 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( A. w e. A B <_ w <-> -. E. w e. A w < B ) )
21 6 11 20 3bitr4d 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B <_ inf ( A , RR , < ) <-> A. w e. A B <_ w ) )
22 breq2 
 |-  ( w = z -> ( B <_ w <-> B <_ z ) )
23 22 cbvralvw 
 |-  ( A. w e. A B <_ w <-> A. z e. A B <_ z )
24 21 23 bitrdi 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( B <_ inf ( A , RR , < ) <-> A. z e. A B <_ z ) )