Theorem suprlubrd

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

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

Proof

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