Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ressioosup.a 
 |-  ( ph -> A C_ RR )
2 ressioosup.s 
 |-  S = sup ( A , RR* , < )
3 ressioosup.n 
 |-  ( ph -> -. S e. A )
4 ressioosup.i 
 |-  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 1 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ RR )
14 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
15 13 14 sseldd 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
16 15 mnfltd 
 |-  ( ( ph /\ x e. A ) -> -oo < x )
17 9 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR* )
18 supxrub 
 |-  ( ( A C_ RR* /\ x e. A ) -> x <_ sup ( A , RR* , < ) )
19 10 14 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 id 
 |-  ( x = S -> x = S )
24 23 eqcomd 
 |-  ( x = S -> S = x )
25 24 adantl 
 |-  ( ( x e. A /\ x = S ) -> S = x )
26 simpl 
 |-  ( ( x e. A /\ x = S ) -> x e. A )
27 25 26 eqeltrd 
 |-  ( ( x e. A /\ x = S ) -> S e. A )
28 27 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ x = S ) -> S e. A )
29 3 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ x = S ) -> -. S e. A )
30 28 29 pm2.65da 
 |-  ( ( ph /\ x e. A ) -> -. x = S )
31 30 neqned 
 |-  ( ( ph /\ x e. A ) -> x =/= S )
32 17 12 22 31 xrleneltd 
 |-  ( ( ph /\ x e. A ) -> x < S )
33 6 12 15 16 32 eliood 
 |-  ( ( ph /\ x e. A ) -> x e. ( -oo (,) S ) )
34 33 4 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> x e. I )
35 34 ralrimiva 
 |-  ( ph -> A. x e. A x e. I )
36 dfss3 
 |-  ( A C_ I <-> A. x e. A x e. I )
37 35 36 sylibr 
 |-  ( ph -> A C_ I )