ressioosup

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

	Ref	Expression
Hypotheses	ressioosup.a	$⊢ φ \to A \subseteq ℝ$
	ressioosup.s	$⊢ S = sup (A ℝ^{*} <)$
	ressioosup.n	$⊢ φ \to \neg S \in A$
	ressioosup.i	$⊢ I = (−∞, S)$
Assertion	ressioosup	$⊢ φ \to A \subseteq I$

Proof

Step	Hyp	Ref	Expression
1		ressioosup.a	$⊢ φ \to A \subseteq ℝ$
2		ressioosup.s	$⊢ S = sup (A ℝ^{*} <)$
3		ressioosup.n	$⊢ φ \to \neg S \in A$
4		ressioosup.i	$⊢ 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	1	adantr	$⊢ (φ \land x \in A) \to A \subseteq ℝ$
14		simpr	$⊢ (φ \land x \in A) \to x \in A$
15	13 14	sseldd	$⊢ (φ \land x \in A) \to x \in ℝ$
16	15	mnfltd	$⊢ (φ \land x \in A) \to −∞ < x$
17	9	sselda	$⊢ (φ \land x \in A) \to x \in ℝ^{*}$
18		supxrub	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \leq sup (A ℝ^{} <)$
19	10 14 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		id	$⊢ x = S \to x = S$
24	23	eqcomd	$⊢ x = S \to S = x$
25	24	adantl	$⊢ (x \in A \land x = S) \to S = x$
26		simpl	$⊢ (x \in A \land x = S) \to x \in A$
27	25 26	eqeltrd	$⊢ (x \in A \land x = S) \to S \in A$
28	27	adantll	$⊢ ((φ \land x \in A) \land x = S) \to S \in A$
29	3	ad2antrr	$⊢ ((φ \land x \in A) \land x = S) \to \neg S \in A$
30	28 29	pm2.65da	$⊢ (φ \land x \in A) \to \neg x = S$
31	30	neqned	$⊢ (φ \land x \in A) \to x \neq S$
32	17 12 22 31	xrleneltd	$⊢ (φ \land x \in A) \to x < S$
33	6 12 15 16 32	eliood	$⊢ (φ \land x \in A) \to x \in (−∞, S)$
34	33 4	eleqtrrdi	$⊢ (φ \land x \in A) \to x \in I$
35	34	ralrimiva	$⊢ φ \to \forall x \in A x \in I$
36		dfss3	$⊢ A \subseteq I \leftrightarrow \forall x \in A x \in I$
37	35 36	sylibr	$⊢ φ \to A \subseteq I$

Metamath Proof Explorer

Theorem ressioosup

Proof