Metamath Proof Explorer


Theorem lbcl

Description: If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion 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 )

Proof

Step Hyp Ref Expression
1 lbreu
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )
2 riotacl
 |-  ( 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 syl
 |-  ( ( 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 )