Theorem ressioosup

Description: If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	ressioosup.a	$$⊢\phi \to A\subseteq ℝ$$
	ressioosup.s	$$⊢S=sup\left(A,{ℝ}^{*},<\right)$$
	ressioosup.n	$$⊢\phi \to \neg S\in A$$
	ressioosup.i	$$⊢I=\left(\mathrm{-\infty },S\right)$$
Assertion	ressioosup	$$⊢\phi \to A\subseteq I$$

Proof

Step	Hyp	Ref	Expression
1		ressioosup.a	$$⊢\phi \to A\subseteq ℝ$$
2		ressioosup.s	$$⊢S=sup\left(A,{ℝ}^{*},<\right)$$
3		ressioosup.n	$$⊢\phi \to \neg S\in A$$
4		ressioosup.i	$$⊢I=\left(\mathrm{-\infty },S\right)$$
5		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
6	5	a1i	$$⊢\left(\phi \wedge x\in A\right)\to \mathrm{-\infty }\in {ℝ}^{*}$$
7		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
8	7	a1i	$$⊢\phi \to ℝ\subseteq {ℝ}^{*}$$
9	1 8	sstrd	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
10	9	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\subseteq {ℝ}^{*}$$
11	10	supxrcld	$$⊢\left(\phi \wedge x\in A\right)\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
12	2 11	eqeltrid	$$⊢\left(\phi \wedge x\in A\right)\to S\in {ℝ}^{*}$$
13	1	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\subseteq ℝ$$
14		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
15	13 14	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to x\in ℝ$$
16	15	mnfltd	$$⊢\left(\phi \wedge x\in A\right)\to \mathrm{-\infty }<x$$
17	9	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in {ℝ}^{*}$$
18		supxrub	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in A\right)\to x\le sup\left(A,{ℝ}^{*},<\right)$$
19	10 14 18	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to x\le sup\left(A,{ℝ}^{*},<\right)$$
20	2	a1i	$$⊢\left(\phi \wedge x\in A\right)\to S=sup\left(A,{ℝ}^{*},<\right)$$
21	20	eqcomd	$$⊢\left(\phi \wedge x\in A\right)\to sup\left(A,{ℝ}^{*},<\right)=S$$
22	19 21	breqtrd	$$⊢\left(\phi \wedge x\in A\right)\to x\le S$$
23		id	$$⊢x=S\to x=S$$
24	23	eqcomd	$$⊢x=S\to S=x$$
25	24	adantl	$$⊢\left(x\in A\wedge x=S\right)\to S=x$$
26		simpl	$$⊢\left(x\in A\wedge x=S\right)\to x\in A$$
27	25 26	eqeltrd	$$⊢\left(x\in A\wedge x=S\right)\to S\in A$$
28	27	adantll	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge x=S\right)\to S\in A$$
29	3	ad2antrr	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge x=S\right)\to \neg S\in A$$
30	28 29	pm2.65da	$$⊢\left(\phi \wedge x\in A\right)\to \neg x=S$$
31	30	neqned	$$⊢\left(\phi \wedge x\in A\right)\to x\ne S$$
32	17 12 22 31	xrleneltd	$$⊢\left(\phi \wedge x\in A\right)\to x<S$$
33	6 12 15 16 32	eliood	$$⊢\left(\phi \wedge x\in A\right)\to x\in \left(\mathrm{-\infty },S\right)$$
34	33 4	eleqtrrdi	$$⊢\left(\phi \wedge x\in A\right)\to x\in I$$
35	34	ralrimiva	$$⊢\phi \to \forall x\in Ax\in I$$
36		dfss3	$$⊢A\subseteq I\leftrightarrow \forall x\in Ax\in I$$
37	35 36	sylibr	$$⊢\phi \to A\subseteq I$$