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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ressioosup.s	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
	ressioosup.n	⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
	ressioosup.i	⊢ 𝐼 = ( -∞ (,) 𝑆 )
Assertion	ressioosup	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ressioosup.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ressioosup.s	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
3		ressioosup.n	⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
4		ressioosup.i	⊢ 𝐼 = ( -∞ (,) 𝑆 )
5		mnfxr	⊢ -∞ ∈ ℝ*
6	5	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ ∈ ℝ* )
7		ressxr	⊢ ℝ ⊆ ℝ*
8	7	a1i	⊢ ( 𝜑 → ℝ ⊆ ℝ* )
9	1 8	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
11	10	supxrcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
12	2 11	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ ℝ* )
13	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
15	13 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
16	15	mnfltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ < 𝑥 )
17	9	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
18		supxrub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
19	10 14 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
20	2	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 = sup ( 𝐴 , ℝ* , < ) )
21	20	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = 𝑆 )
22	19 21	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝑆 )
23		id	⊢ ( 𝑥 = 𝑆 → 𝑥 = 𝑆 )
24	23	eqcomd	⊢ ( 𝑥 = 𝑆 → 𝑆 = 𝑥 )
25	24	adantl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 = 𝑥 )
26		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑥 ∈ 𝐴 )
27	25 26	eqeltrd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
28	27	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
29	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → ¬ 𝑆 ∈ 𝐴 )
30	28 29	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝑆 )
31	30	neqned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ 𝑆 )
32	17 12 22 31	xrleneltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 < 𝑆 )
33	6 12 15 16 32	eliood	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( -∞ (,) 𝑆 ) )
34	33 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐼 )
35	34	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
36		dfss3	⊢ ( 𝐴 ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
37	35 36	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )