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 )

Step

Hyp

Ref

Expression

lbreu

 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )

riotacl

 |-  ( E! x e. S A. y e. S x <_ y -> ( iota_ x e. S A. y e. S x <_ y ) e. S )

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 )