Metamath Proof Explorer


Theorem lbinfcl

Description: If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion lbinfcl
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) e. S )

Proof

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 lbcl
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. S )
3 1 2 eqeltrd
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) e. S )