Metamath Proof Explorer

Theorem infmrgelbi

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013) (Revised by AV, 17-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> A. x e. A B <_ x )
2 simpl1 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> A C_ RR )
3 simpl2 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> A =/= (/) )
4 breq1 
 |-  ( z = B -> ( z <_ x <-> B <_ x ) )
5 4 ralbidv 
 |-  ( z = B -> ( A. x e. A z <_ x <-> A. x e. A B <_ x ) )
6 5 rspcev 
 |-  ( ( B e. RR /\ A. x e. A B <_ x ) -> E. z e. RR A. x e. A z <_ x )
7 6 3ad2antl3 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> E. z e. RR A. x e. A z <_ x )
8 simpl3 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> B e. RR )
9 infregelb 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. z e. RR A. x e. A z <_ x ) /\ B e. RR ) -> ( B <_ inf ( A , RR , < ) <-> A. x e. A B <_ x ) )
10 2 3 7 8 9 syl31anc 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> ( B <_ inf ( A , RR , < ) <-> A. x e. A B <_ x ) )
11 1 10 mpbird 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> B <_ inf ( A , RR , < ) )