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