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	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℝ* )
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 ( 𝑆 , ℝ* , < ) ∈ ( 𝐴 [,] 𝐵 ) )