Metamath Proof Explorer

Theorem inficc

Description: The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses inficc.a 
|- ( ph -> A e. RR* )
inficc.b 
|- ( ph -> B e. RR* )
inficc.s 
|- ( ph -> S C_ ( A [,] B ) )
inficc.n0 
|- ( ph -> S =/= (/) )
Assertion inficc 
|- ( ph -> inf ( S , RR* , < ) e. ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 inficc.a 
 |-  ( ph -> A e. RR* )
2 inficc.b 
 |-  ( ph -> B e. RR* )
3 inficc.s 
 |-  ( ph -> S C_ ( A [,] B ) )
4 inficc.n0 
 |-  ( ph -> S =/= (/) )
5 iccssxr 
 |-  ( A [,] B ) C_ RR*
6 5 a1i 
 |-  ( ph -> ( A [,] B ) C_ RR* )
7 3 6 sstrd 
 |-  ( ph -> S C_ RR* )
8 infxrcl 
 |-  ( S C_ RR* -> inf ( S , RR* , < ) e. RR* )
9 7 8 syl 
 |-  ( ph -> inf ( S , RR* , < ) e. RR* )
10 1 adantr 
 |-  ( ( ph /\ x e. S ) -> A e. RR* )
11 2 adantr 
 |-  ( ( ph /\ x e. S ) -> B e. RR* )
12 3 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. ( A [,] B ) )
13 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> A <_ x )
14 10 11 12 13 syl3anc 
 |-  ( ( ph /\ x e. S ) -> A <_ x )
15 14 ralrimiva 
 |-  ( ph -> A. x e. S A <_ x )
16 infxrgelb 
 |-  ( ( S C_ RR* /\ A e. RR* ) -> ( A <_ inf ( S , RR* , < ) <-> A. x e. S A <_ x ) )
17 7 1 16 syl2anc 
 |-  ( ph -> ( A <_ inf ( S , RR* , < ) <-> A. x e. S A <_ x ) )
18 15 17 mpbird 
 |-  ( ph -> A <_ inf ( S , RR* , < ) )
19 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
20 4 19 sylib 
 |-  ( ph -> E. x x e. S )
21 9 adantr 
 |-  ( ( ph /\ x e. S ) -> inf ( S , RR* , < ) e. RR* )
22 5 12 sselid 
 |-  ( ( ph /\ x e. S ) -> x e. RR* )
23 7 adantr 
 |-  ( ( ph /\ x e. S ) -> S C_ RR* )
24 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
25 infxrlb 
 |-  ( ( S C_ RR* /\ x e. S ) -> inf ( S , RR* , < ) <_ x )
26 23 24 25 syl2anc 
 |-  ( ( ph /\ x e. S ) -> inf ( S , RR* , < ) <_ x )
27 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> x <_ B )
28 10 11 12 27 syl3anc 
 |-  ( ( ph /\ x e. S ) -> x <_ B )
29 21 22 11 26 28 xrletrd 
 |-  ( ( ph /\ x e. S ) -> inf ( S , RR* , < ) <_ B )
30 29 ex 
 |-  ( ph -> ( x e. S -> inf ( S , RR* , < ) <_ B ) )
31 30 exlimdv 
 |-  ( ph -> ( E. x x e. S -> inf ( S , RR* , < ) <_ B ) )
32 20 31 mpd 
 |-  ( ph -> inf ( S , RR* , < ) <_ B )
33 1 2 9 18 32 eliccxrd 
 |-  ( ph -> inf ( S , RR* , < ) e. ( A [,] B ) )