Description: If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lbinfle | |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> inf ( S , RR , < ) <_ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lbinf | |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) ) |
|
| 2 | 1 | 3adant3 | |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) ) |
| 3 | lble | |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A ) |
|
| 4 | 2 3 | eqbrtrd | |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> inf ( S , RR , < ) <_ A ) |