Theorem suprcld

Description: Natural deduction form of suprcl . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	suprcld.2	|- ( ph -> A C_ RR )
	suprcld.1	|- ( ph -> A =/= (/) )
	suprcld.4	|- ( ph -> E. x e. RR A. y e. A y <_ x )
Assertion	suprcld	|- ( ph -> sup ( A , RR , < ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		suprcld.2	|- ( ph -> A C_ RR )
2		suprcld.1	|- ( ph -> A =/= (/) )
3		suprcld.4	|- ( ph -> E. x e. RR A. y e. A y <_ x )
4		suprcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
5	1 2 3 4	syl3anc	|- ( ph -> sup ( A , RR , < ) e. RR )