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	|- ( ph -> A C_ RR )
	ressiocsup.s	|- S = sup ( A , RR* , < )
	ressiocsup.e	|- ( ph -> S e. A )
	ressiocsup.5	|- I = ( -oo (,] S )
Assertion	ressiocsup	|- ( ph -> A C_ I )

Proof

Step	Hyp	Ref	Expression
1		ressiocsup.a	|- ( ph -> A C_ RR )
2		ressiocsup.s	|- S = sup ( A , RR* , < )
3		ressiocsup.e	|- ( ph -> S e. A )
4		ressiocsup.5	|- I = ( -oo (,] S )
5		mnfxr	|- -oo e. RR*
6	5	a1i	|- ( ( ph /\ x e. A ) -> -oo e. RR* )
7		ressxr	|- RR C_ RR*
8	7	a1i	|- ( ph -> RR C_ RR* )
9	1 8	sstrd	|- ( ph -> A C_ RR* )
10	9	adantr	|- ( ( ph /\ x e. A ) -> A C_ RR* )
11	10	supxrcld	|- ( ( ph /\ x e. A ) -> sup ( A , RR* , < ) e. RR* )
12	2 11	eqeltrid	|- ( ( ph /\ x e. A ) -> S e. RR* )
13	9	sselda	|- ( ( ph /\ x e. A ) -> x e. RR* )
14	1	adantr	|- ( ( ph /\ x e. A ) -> A C_ RR )
15		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
16	14 15	sseldd	|- ( ( ph /\ x e. A ) -> x e. RR )
17	16	mnfltd	|- ( ( ph /\ x e. A ) -> -oo < x )
18		supxrub	|- ( ( A C_ RR* /\ x e. A ) -> x <_ sup ( A , RR* , < ) )
19	10 15 18	syl2anc	|- ( ( ph /\ x e. A ) -> x <_ sup ( A , RR* , < ) )
20	2	a1i	|- ( ( ph /\ x e. A ) -> S = sup ( A , RR* , < ) )
21	20	eqcomd	|- ( ( ph /\ x e. A ) -> sup ( A , RR* , < ) = S )
22	19 21	breqtrd	|- ( ( ph /\ x e. A ) -> x <_ S )
23	6 12 13 17 22	eliocd	|- ( ( ph /\ x e. A ) -> x e. ( -oo (,] S ) )
24	23 4	eleqtrrdi	|- ( ( ph /\ x e. A ) -> x e. I )
25	24	ralrimiva	|- ( ph -> A. x e. A x e. I )
26		dfss3	|- ( A C_ I <-> A. x e. A x e. I )
27	25 26	sylibr	|- ( ph -> A C_ I )