Theorem ubelsupr

Description: If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> A C_ RR )
2		simp2	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> U e. A )
3	2	ne0d	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> A =/= (/) )
4	1 2	sseldd	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> U e. RR )
5		simp3	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> A. x e. A x <_ U )
6		brralrspcev	|- ( ( U e. RR /\ A. x e. A x <_ U ) -> E. y e. RR A. x e. A x <_ y )
7	4 5 6	syl2anc	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> E. y e. RR A. x e. A x <_ y )
8	1 3 7	3jca	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. x e. A x <_ y ) )
9		suprub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. x e. A x <_ y ) /\ U e. A ) -> U <_ sup ( A , RR , < ) )
10	8 2 9	syl2anc	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> U <_ sup ( A , RR , < ) )
11		suprleub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. x e. A x <_ y ) /\ U e. RR ) -> ( sup ( A , RR , < ) <_ U <-> A. x e. A x <_ U ) )
12	8 4 11	syl2anc	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> ( sup ( A , RR , < ) <_ U <-> A. x e. A x <_ U ) )
13	5 12	mpbird	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> sup ( A , RR , < ) <_ U )
14		suprcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. x e. A x <_ y ) -> sup ( A , RR , < ) e. RR )
15	8 14	syl	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> sup ( A , RR , < ) e. RR )
16	4 15	letri3d	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> ( U = sup ( A , RR , < ) <-> ( U <_ sup ( A , RR , < ) /\ sup ( A , RR , < ) <_ U ) ) )
17	10 13 16	mpbir2and	|- ( ( A C_ RR /\ U e. A /\ A. x e. A x <_ U ) -> U = sup ( A , RR , < ) )