This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )