Theorem ressiocsup

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

	Ref	Expression
Hypotheses	ressiocsup.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ressiocsup.s	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
	ressiocsup.e	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
	ressiocsup.5	⊢ 𝐼 = ( -∞ (,] 𝑆 )
Assertion	ressiocsup	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ressiocsup.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ressiocsup.s	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
3		ressiocsup.e	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
4		ressiocsup.5	⊢ 𝐼 = ( -∞ (,] 𝑆 )
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	9	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
14	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
16	14 15	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
17	16	mnfltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ < 𝑥 )
18		supxrub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
19	10 15 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ* , < ) )
20	2	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 = sup ( 𝐴 , ℝ* , < ) )
21	20	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = 𝑆 )
22	19 21	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝑆 )
23	6 12 13 17 22	eliocd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( -∞ (,] 𝑆 ) )
24	23 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐼 )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
26		dfss3	⊢ ( 𝐴 ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
27	25 26	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )