Theorem ressiooinf

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

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

Proof

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