This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , < ) )