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

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
inficc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
inficc.s ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
inficc.n0 ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
Assertion inficc ( 𝜑 → inf ( 𝑆 , ℝ* , < ) ∈ ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 inficc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 inficc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 inficc.s ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
4 inficc.n0 ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
5 iccssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
6 5 a1i ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ* )
7 3 6 sstrd ⊢ ( 𝜑 → 𝑆 ⊆ ℝ* )
8 infxrcl ⊢ ( 𝑆 ⊆ ℝ* → inf ( 𝑆 , ℝ* , < ) ∈ ℝ* )
9 7 8 syl ⊢ ( 𝜑 → inf ( 𝑆 , ℝ* , < ) ∈ ℝ* )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ* )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ* )
12 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
13 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
14 10 11 12 13 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ≤ 𝑥 )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ≤ 𝑥 )
16 infxrgelb ⊢ ( ( 𝑆 ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ inf ( 𝑆 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝑆 𝐴 ≤ 𝑥 ) )
17 7 1 16 syl2anc ⊢ ( 𝜑 → ( 𝐴 ≤ inf ( 𝑆 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝑆 𝐴 ≤ 𝑥 ) )
18 15 17 mpbird ⊢ ( 𝜑 → 𝐴 ≤ inf ( 𝑆 , ℝ* , < ) )
19 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
20 4 19 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝑆 )
21 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → inf ( 𝑆 , ℝ* , < ) ∈ ℝ* )
22 5 12 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℝ* )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ℝ* )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
25 infxrlb ⊢ ( ( 𝑆 ⊆ ℝ* ∧ 𝑥 ∈ 𝑆 ) → inf ( 𝑆 , ℝ* , < ) ≤ 𝑥 )
26 23 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → inf ( 𝑆 , ℝ* , < ) ≤ 𝑥 )
27 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
28 10 11 12 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≤ 𝐵 )
29 21 22 11 26 28 xrletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → inf ( 𝑆 , ℝ* , < ) ≤ 𝐵 )
30 29 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → inf ( 𝑆 , ℝ* , < ) ≤ 𝐵 ) )
31 30 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ 𝑆 → inf ( 𝑆 , ℝ* , < ) ≤ 𝐵 ) )
32 20 31 mpd ⊢ ( 𝜑 → inf ( 𝑆 , ℝ* , < ) ≤ 𝐵 )
33 1 2 9 18 32 eliccxrd ⊢ ( 𝜑 → inf ( 𝑆 , ℝ* , < ) ∈ ( 𝐴 [,] 𝐵 ) )