Theorem suprcl

Description: Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004)

	Ref	Expression
Assertion	suprcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		ltso	|- < Or RR
2	1	a1i	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> < Or RR )
3		sup3	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
4	2 3	supcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )