Theorem supiccub

Description: The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-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$$
Assertion	supiccub	$$⊢\phi \to D\le sup\left(A,ℝ,<\right)$$

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		iccssre	$$⊢\left(B\in ℝ\wedge C\in ℝ\right)\to \left[B,C\right]\subseteq ℝ$$
7	1 2 6	syl2anc	$$⊢\phi \to \left[B,C\right]\subseteq ℝ$$
8	3 7	sstrd	$$⊢\phi \to A\subseteq ℝ$$
9	1	adantr	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
10	9	rexrd	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
11	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
12	11	rexrd	$$⊢\left(\phi \wedge x\in A\right)\to C\in {ℝ}^{*}$$
13	3	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in \left[B,C\right]$$
14		iccleub	$$⊢\left(B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\wedge x\in \left[B,C\right]\right)\to x\le C$$
15	10 12 13 14	syl3anc	$$⊢\left(\phi \wedge x\in A\right)\to x\le C$$
16	15	ralrimiva	$$⊢\phi \to \forall x\in Ax\le C$$
17		brralrspcev	$$⊢\left(C\in ℝ\wedge \forall x\in Ax\le C\right)\to \exists y\in ℝ\forall x\in Ax\le y$$
18	2 16 17	syl2anc	$$⊢\phi \to \exists y\in ℝ\forall x\in Ax\le y$$
19	8 4 18 5	suprubd	$$⊢\phi \to D\le sup\left(A,ℝ,<\right)$$