Theorem supicclub2

Description: The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019)

	Ref	Expression
Hypotheses	supicc.1	|- ( ph -> B e. RR )
	supicc.2	|- ( ph -> C e. RR )
	supicc.3	|- ( ph -> A C_ ( B [,] C ) )
	supicc.4	|- ( ph -> A =/= (/) )
	supiccub.1	|- ( ph -> D e. A )
	supicclub2.1	|- ( ( ph /\ z e. A ) -> z <_ D )
Assertion	supicclub2	|- ( ph -> sup ( A , RR , < ) <_ D )

Proof

Step	Hyp	Ref	Expression
1		supicc.1	|- ( ph -> B e. RR )
2		supicc.2	|- ( ph -> C e. RR )
3		supicc.3	|- ( ph -> A C_ ( B [,] C ) )
4		supicc.4	|- ( ph -> A =/= (/) )
5		supiccub.1	|- ( ph -> D e. A )
6		supicclub2.1	|- ( ( ph /\ z e. A ) -> z <_ D )
7		iccssxr	|- ( B [,] C ) C_ RR*
8	1 2 3 4	supicc	|- ( ph -> sup ( A , RR , < ) e. ( B [,] C ) )
9	7 8	sselid	|- ( ph -> sup ( A , RR , < ) e. RR* )
10	3 7	sstrdi	|- ( ph -> A C_ RR* )
11	10 5	sseldd	|- ( ph -> D e. RR* )
12	10	sselda	|- ( ( ph /\ z e. A ) -> z e. RR* )
13	11	adantr	|- ( ( ph /\ z e. A ) -> D e. RR* )
14	12 13	xrlenltd	|- ( ( ph /\ z e. A ) -> ( z <_ D <-> -. D < z ) )
15	6 14	mpbid	|- ( ( ph /\ z e. A ) -> -. D < z )
16	15	nrexdv	|- ( ph -> -. E. z e. A D < z )
17	1 2 3 4 5	supicclub	|- ( ph -> ( D < sup ( A , RR , < ) <-> E. z e. A D < z ) )
18	16 17	mtbird	|- ( ph -> -. D < sup ( A , RR , < ) )
19	9 11 18	xrnltled	|- ( ph -> sup ( A , RR , < ) <_ D )