ressiocsup

Description: If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	ressiocsup.a	$⊢ φ \to A \subseteq ℝ$
	ressiocsup.s	$⊢ S = sup (A ℝ^{*} <)$
	ressiocsup.e	$⊢ φ \to S \in A$
	ressiocsup.5	$⊢ I = (−∞, S]$
Assertion	ressiocsup	$⊢ φ \to A \subseteq I$

Proof

Step	Hyp	Ref	Expression
1		ressiocsup.a	$⊢ φ \to A \subseteq ℝ$
2		ressiocsup.s	$⊢ S = sup (A ℝ^{*} <)$
3		ressiocsup.e	$⊢ φ \to S \in A$
4		ressiocsup.5	$⊢ I = (−∞, S]$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6	5	a1i	$⊢ (φ \land x \in A) \to −∞ \in ℝ^{*}$
7		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
8	7	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
9	1 8	sstrd	$⊢ φ \to A \subseteq ℝ^{*}$
10	9	adantr	$⊢ (φ \land x \in A) \to A \subseteq ℝ^{*}$
11	10	supxrcld	$⊢ (φ \land x \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
12	2 11	eqeltrid	$⊢ (φ \land x \in A) \to S \in ℝ^{*}$
13	9	sselda	$⊢ (φ \land x \in A) \to x \in ℝ^{*}$
14	1	adantr	$⊢ (φ \land x \in A) \to A \subseteq ℝ$
15		simpr	$⊢ (φ \land x \in A) \to x \in A$
16	14 15	sseldd	$⊢ (φ \land x \in A) \to x \in ℝ$
17	16	mnfltd	$⊢ (φ \land x \in A) \to −∞ < x$
18		supxrub	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \leq sup (A ℝ^{} <)$
19	10 15 18	syl2anc	$⊢ (φ \land x \in A) \to x \leq sup (A ℝ^{*} <)$
20	2	a1i	$⊢ (φ \land x \in A) \to S = sup (A ℝ^{*} <)$
21	20	eqcomd	$⊢ (φ \land x \in A) \to sup (A ℝ^{*} <) = S$
22	19 21	breqtrd	$⊢ (φ \land x \in A) \to x \leq S$
23	6 12 13 17 22	eliocd	$⊢ (φ \land x \in A) \to x \in (−∞, S]$
24	23 4	eleqtrrdi	$⊢ (φ \land x \in A) \to x \in I$
25	24	ralrimiva	$⊢ φ \to \forall x \in A x \in I$
26		dfss3	$⊢ A \subseteq I \leftrightarrow \forall x \in A x \in I$
27	25 26	sylibr	$⊢ φ \to A \subseteq I$

Metamath Proof Explorer

Theorem ressiocsup

Proof