infxrlesupxr

Description: The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infxrlesupxr.1	$⊢ φ \to A \subseteq ℝ^{*}$
	infxrlesupxr.2	$⊢ φ \to A \neq \emptyset$
Assertion	infxrlesupxr	$⊢ φ \to inf (A ℝ^{} <) \leq sup (A ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		infxrlesupxr.1	$⊢ φ \to A \subseteq ℝ^{*}$
2		infxrlesupxr.2	$⊢ φ \to A \neq \emptyset$
3		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
4	3	biimpi	$⊢ A \neq \emptyset \to \exists x x \in A$
5	2 4	syl	$⊢ φ \to \exists x x \in A$
6	1	infxrcld	$⊢ φ \to inf (A ℝ^{} <) \in ℝ^{}$
7	6	adantr	$⊢ (φ \land x \in A) \to inf (A ℝ^{} <) \in ℝ^{}$
8	1	sselda	$⊢ (φ \land x \in A) \to x \in ℝ^{*}$
9	1	supxrcld	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
10	9	adantr	$⊢ (φ \land x \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
11	1	adantr	$⊢ (φ \land x \in A) \to A \subseteq ℝ^{*}$
12		simpr	$⊢ (φ \land x \in A) \to x \in A$
13		infxrlb	$⊢ (A \subseteq ℝ^{} \land x \in A) \to inf (A ℝ^{} <) \leq x$
14	11 12 13	syl2anc	$⊢ (φ \land x \in A) \to inf (A ℝ^{*} <) \leq x$
15		eqid	$⊢ sup (A ℝ^{} <) = sup (A ℝ^{} <)$
16	11 12 15	supxrubd	$⊢ (φ \land x \in A) \to x \leq sup (A ℝ^{*} <)$
17	7 8 10 14 16	xrletrd	$⊢ (φ \land x \in A) \to inf (A ℝ^{} <) \leq sup (A ℝ^{} <)$
18	17	ex	$⊢ φ \to (x \in A \to inf (A ℝ^{} <) \leq sup (A ℝ^{} <))$
19	18	exlimdv	$⊢ φ \to (\exists x x \in A \to inf (A ℝ^{} <) \leq sup (A ℝ^{} <))$
20	5 19	mpd	$⊢ φ \to inf (A ℝ^{} <) \leq sup (A ℝ^{} <)$

Metamath Proof Explorer

Theorem infxrlesupxr

Proof