Theorem suprleubrd

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

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

Proof

Step	Hyp	Ref	Expression
1		suprleubrd.1	|- ( ph -> A C_ RR )
2		suprleubrd.2	|- ( ph -> A =/= (/) )
3		suprleubrd.3	|- ( ph -> E. x e. RR A. y e. A y <_ x )
4		suprleubrd.4	|- ( ph -> B e. RR )
5		suprleubrd.5	|- ( ph -> A. z e. A z <_ B )
6		suprleub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
7	1 2 3 4 6	syl31anc	|- ( ph -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
8	7	bicomd	|- ( ph -> ( A. z e. A z <_ B <-> sup ( A , RR , < ) <_ B ) )
9	8	biimpd	|- ( ph -> ( A. z e. A z <_ B -> sup ( A , RR , < ) <_ B ) )
10	9	imp	|- ( ( ph /\ A. z e. A z <_ B ) -> sup ( A , RR , < ) <_ B )
11	5 10	mpdan	|- ( ph -> sup ( A , RR , < ) <_ B )