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