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	$⊢ φ \to A \in ℝ^{*}$
	inficc.b	$⊢ φ \to B \in ℝ^{*}$
	inficc.s	$⊢ φ \to S \subseteq [A, B]$
	inficc.n0	$⊢ φ \to S \neq \emptyset$
Assertion	inficc	$⊢ φ \to inf (S ℝ^{*} <) \in [A, B]$

Proof

Step	Hyp	Ref	Expression
1		inficc.a	$⊢ φ \to A \in ℝ^{*}$
2		inficc.b	$⊢ φ \to B \in ℝ^{*}$
3		inficc.s	$⊢ φ \to S \subseteq [A, B]$
4		inficc.n0	$⊢ φ \to S \neq \emptyset$
5		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
6	5	a1i	$⊢ φ \to [A, B] \subseteq ℝ^{*}$
7	3 6	sstrd	$⊢ φ \to S \subseteq ℝ^{*}$
8		infxrcl	$⊢ S \subseteq ℝ^{} \to inf (S ℝ^{} <) \in ℝ^{*}$
9	7 8	syl	$⊢ φ \to inf (S ℝ^{} <) \in ℝ^{}$
10	1	adantr	$⊢ (φ \land x \in S) \to A \in ℝ^{*}$
11	2	adantr	$⊢ (φ \land x \in S) \to B \in ℝ^{*}$
12	3	sselda	$⊢ (φ \land x \in S) \to x \in [A, B]$
13		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to A \leq x$
14	10 11 12 13	syl3anc	$⊢ (φ \land x \in S) \to A \leq x$
15	14	ralrimiva	$⊢ φ \to \forall x \in S A \leq x$
16		infxrgelb	$⊢ (S \subseteq ℝ^{} \land A \in ℝ^{}) \to (A \leq inf (S ℝ^{*} <) \leftrightarrow \forall x \in S A \leq x)$
17	7 1 16	syl2anc	$⊢ φ \to (A \leq inf (S ℝ^{*} <) \leftrightarrow \forall x \in S A \leq x)$
18	15 17	mpbird	$⊢ φ \to A \leq inf (S ℝ^{*} <)$
19		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
20	4 19	sylib	$⊢ φ \to \exists x x \in S$
21	9	adantr	$⊢ (φ \land x \in S) \to inf (S ℝ^{} <) \in ℝ^{}$
22	5 12	sselid	$⊢ (φ \land x \in S) \to x \in ℝ^{*}$
23	7	adantr	$⊢ (φ \land x \in S) \to S \subseteq ℝ^{*}$
24		simpr	$⊢ (φ \land x \in S) \to x \in S$
25		infxrlb	$⊢ (S \subseteq ℝ^{} \land x \in S) \to inf (S ℝ^{} <) \leq x$
26	23 24 25	syl2anc	$⊢ (φ \land x \in S) \to inf (S ℝ^{*} <) \leq x$
27		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
28	10 11 12 27	syl3anc	$⊢ (φ \land x \in S) \to x \leq B$
29	21 22 11 26 28	xrletrd	$⊢ (φ \land x \in S) \to inf (S ℝ^{*} <) \leq B$
30	29	ex	$⊢ φ \to (x \in S \to inf (S ℝ^{*} <) \leq B)$
31	30	exlimdv	$⊢ φ \to (\exists x x \in S \to inf (S ℝ^{*} <) \leq B)$
32	20 31	mpd	$⊢ φ \to inf (S ℝ^{*} <) \leq B$
33	1 2 9 18 32	eliccxrd	$⊢ φ \to inf (S ℝ^{*} <) \in [A, B]$

Metamath Proof Explorer

Theorem inficc

Proof