Theorem suprubd

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

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

Proof

Step	Hyp	Ref	Expression
1		suprubd.1	|- ( ph -> A C_ RR )
2		suprubd.2	|- ( ph -> A =/= (/) )
3		suprubd.3	|- ( ph -> E. x e. RR A. y e. A y <_ x )
4		suprubd.4	|- ( ph -> B e. A )
5		suprub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. A ) -> B <_ sup ( A , RR , < ) )
6	1 2 3 4 5	syl31anc	|- ( ph -> B <_ sup ( A , RR , < ) )