Metamath Proof Explorer

Theorem ressiooinf

Description: If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ressiooinf.a 
|- ( ph -> A C_ RR )
ressiooinf.s 
|- S = inf ( A , RR* , < )
ressiooinf.n 
|- ( ph -> -. S e. A )
ressiooinf.i 
|- I = ( S (,) +oo )
Assertion ressiooinf 
|- ( ph -> A C_ I )

Proof

Step Hyp Ref Expression
1 ressiooinf.a 
 |-  ( ph -> A C_ RR )
2 ressiooinf.s 
 |-  S = inf ( A , RR* , < )
3 ressiooinf.n 
 |-  ( ph -> -. S e. A )
4 ressiooinf.i 
 |-  I = ( S (,) +oo )
5 ressxr 
 |-  RR C_ RR*
6 5 a1i 
 |-  ( ph -> RR C_ RR* )
7 1 6 sstrd 
 |-  ( ph -> A C_ RR* )
8 7 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ RR* )
9 8 infxrcld 
 |-  ( ( ph /\ x e. A ) -> inf ( A , RR* , < ) e. RR* )
10 2 9 eqeltrid 
 |-  ( ( ph /\ x e. A ) -> S e. RR* )
11 pnfxr 
 |-  +oo e. RR*
12 11 a1i 
 |-  ( ( ph /\ x e. A ) -> +oo 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 7 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR* )
17 infxrlb 
 |-  ( ( A C_ RR* /\ x e. A ) -> inf ( A , RR* , < ) <_ x )
18 8 14 17 syl2anc 
 |-  ( ( ph /\ x e. A ) -> inf ( A , RR* , < ) <_ x )
19 2 18 eqbrtrid 
 |-  ( ( ph /\ x e. A ) -> S <_ x )
20 id 
 |-  ( x = S -> x = S )
21 20 eqcomd 
 |-  ( x = S -> S = x )
22 21 adantl 
 |-  ( ( x e. A /\ x = S ) -> S = x )
23 simpl 
 |-  ( ( x e. A /\ x = S ) -> x e. A )
24 22 23 eqeltrd 
 |-  ( ( x e. A /\ x = S ) -> S e. A )
25 24 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ x = S ) -> S e. A )
26 3 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ x = S ) -> -. S e. A )
27 25 26 pm2.65da 
 |-  ( ( ph /\ x e. A ) -> -. x = S )
28 27 neqned 
 |-  ( ( ph /\ x e. A ) -> x =/= S )
29 28 necomd 
 |-  ( ( ph /\ x e. A ) -> S =/= x )
30 10 16 19 29 xrleneltd 
 |-  ( ( ph /\ x e. A ) -> S < x )
31 15 ltpnfd 
 |-  ( ( ph /\ x e. A ) -> x < +oo )
32 10 12 15 30 31 eliood 
 |-  ( ( ph /\ x e. A ) -> x e. ( S (,) +oo ) )
33 32 4 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> x e. I )
34 33 ralrimiva 
 |-  ( ph -> A. x e. A x e. I )
35 dfss3 
 |-  ( A C_ I <-> A. x e. A x e. I )
36 34 35 sylibr 
 |-  ( ph -> A C_ I )