supxrbnd

Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	supxrbnd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land sup (A ℝ^{} <) < +∞) \to sup (A ℝ^{} <) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
2		sstr	$⊢ (A \subseteq ℝ \land ℝ \subseteq ℝ^{}) \to A \subseteq ℝ^{}$
3	1 2	mpan2	$⊢ A \subseteq ℝ \to A \subseteq ℝ^{*}$
4		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
5		pnfxr	$⊢ +∞ \in ℝ^{*}$
6		xrltne	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land +∞ \in ℝ^{} \land sup (A ℝ^{} <) < +∞) \to +∞ \neq sup (A ℝ^{*} <)$
7	5 6	mp3an2	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land sup (A ℝ^{} <) < +∞) \to +∞ \neq sup (A ℝ^{} <)$
8	7	necomd	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land sup (A ℝ^{} <) < +∞) \to sup (A ℝ^{} <) \neq +∞$
9	8	ex	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) < +∞ \to sup (A ℝ^{} <) \neq +∞)$
10	4 9	syl	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) < +∞ \to sup (A ℝ^{*} <) \neq +∞)$
11		supxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x < y \leftrightarrow sup (A ℝ^{} <) = +∞)$
12		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
13	12	adantlr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \to y \in ℝ^{}$
14		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
15	14	ad2antlr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \to x \in ℝ^{}$
16		xrlenlt	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to (y \leq x \leftrightarrow \neg x < y)$
17	16	con2bid	$⊢ (y \in ℝ^{} \land x \in ℝ^{}) \to (x < y \leftrightarrow \neg y \leq x)$
18	13 15 17	syl2anc	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \to (x < y \leftrightarrow \neg y \leq x)$
19	18	rexbidva	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A x < y \leftrightarrow \exists y \in A \neg y \leq x)$
20		rexnal	$⊢ \exists y \in A \neg y \leq x \leftrightarrow \neg \forall y \in A y \leq x$
21	19 20	bitrdi	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A x < y \leftrightarrow \neg \forall y \in A y \leq x)$
22	21	ralbidva	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \exists y \in A x < y \leftrightarrow \forall x \in ℝ \neg \forall y \in A y \leq x)$
23	11 22	bitr3d	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \forall x \in ℝ \neg \forall y \in A y \leq x)$
24		ralnex	$⊢ \forall x \in ℝ \neg \forall y \in A y \leq x \leftrightarrow \neg \exists x \in ℝ \forall y \in A y \leq x$
25	23 24	bitrdi	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg \exists x \in ℝ \forall y \in A y \leq x)$
26	25	necon2abid	$⊢ A \subseteq ℝ^{} \to (\exists x \in ℝ \forall y \in A y \leq x \leftrightarrow sup (A ℝ^{} <) \neq +∞)$
27	10 26	sylibrd	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) < +∞ \to \exists x \in ℝ \forall y \in A y \leq x)$
28	27	imp	$⊢ (A \subseteq ℝ^{} \land sup (A ℝ^{} <) < +∞) \to \exists x \in ℝ \forall y \in A y \leq x$
29	3 28	sylan	$⊢ (A \subseteq ℝ \land sup (A ℝ^{*} <) < +∞) \to \exists x \in ℝ \forall y \in A y \leq x$
30	29	3adant2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land sup (A ℝ^{*} <) < +∞) \to \exists x \in ℝ \forall y \in A y \leq x$
31		supxrre	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) = sup (A ℝ <)$
32		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
33	31 32	eqeltrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) \in ℝ$
34	30 33	syld3an3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land sup (A ℝ^{} <) < +∞) \to sup (A ℝ^{} <) \in ℝ$

Metamath Proof Explorer

Theorem supxrbnd

Proof