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 )

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 )

Step

Hyp

Ref

Expression

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

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

1 2

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