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	$$⊢\phi \to B\in ℝ$$
	supicc.2	$$⊢\phi \to C\in ℝ$$
	supicc.3	$$⊢\phi \to A\subseteq \left[B,C\right]$$
	supicc.4	$$⊢\phi \to A\ne \varnothing$$
	supiccub.1	$$⊢\phi \to D\in A$$
	supicclub2.1	$$⊢\left(\phi \wedge z\in A\right)\to z\le D$$
Assertion	supicclub2	$$⊢\phi \to sup\left(A,ℝ,<\right)\le D$$

Proof

Step	Hyp	Ref	Expression
1		supicc.1	$$⊢\phi \to B\in ℝ$$
2		supicc.2	$$⊢\phi \to C\in ℝ$$
3		supicc.3	$$⊢\phi \to A\subseteq \left[B,C\right]$$
4		supicc.4	$$⊢\phi \to A\ne \varnothing$$
5		supiccub.1	$$⊢\phi \to D\in A$$
6		supicclub2.1	$$⊢\left(\phi \wedge z\in A\right)\to z\le D$$
7		iccssxr	$$⊢\left[B,C\right]\subseteq {ℝ}^{*}$$
8	1 2 3 4	supicc	$$⊢\phi \to sup\left(A,ℝ,<\right)\in \left[B,C\right]$$
9	7 8	sselid	$$⊢\phi \to sup\left(A,ℝ,<\right)\in {ℝ}^{*}$$
10	3 7	sstrdi	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
11	10 5	sseldd	$$⊢\phi \to D\in {ℝ}^{*}$$
12	10	sselda	$$⊢\left(\phi \wedge z\in A\right)\to z\in {ℝ}^{*}$$
13	11	adantr	$$⊢\left(\phi \wedge z\in A\right)\to D\in {ℝ}^{*}$$
14	12 13	xrlenltd	$$⊢\left(\phi \wedge z\in A\right)\to \left(z\le D\leftrightarrow \neg D<z\right)$$
15	6 14	mpbid	$$⊢\left(\phi \wedge z\in A\right)\to \neg D<z$$
16	15	nrexdv	$$⊢\phi \to \neg \exists z\in AD<z$$
17	1 2 3 4 5	supicclub	$$⊢\phi \to \left(D<sup\left(A,ℝ,<\right)\leftrightarrow \exists z\in AD<z\right)$$
18	16 17	mtbird	$$⊢\phi \to \neg D<sup\left(A,ℝ,<\right)$$
19	9 11 18	xrnltled	$$⊢\phi \to sup\left(A,ℝ,<\right)\le D$$