This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supxrbnd1

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

		Ref	Expression
	Assertion	supxrbnd1	$⊢ A \subseteq ℝ^{} \to (\exists x \in ℝ \forall y \in A y < x \leftrightarrow sup (A ℝ^{} <) < +∞)$

Proof

Step	Hyp	Ref	Expression
1		ralnex	$⊢ \forall x \in ℝ \neg \forall y \in A y < x \leftrightarrow \neg \exists x \in ℝ \forall y \in A y < x$
2		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
3		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
4		xrlenlt	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow \neg y < x)$
5	2 3 4	syl2anr	$⊢ ((A \subseteq ℝ^{*} \land y \in A) \land x \in ℝ) \to (x \leq y \leftrightarrow \neg y < x)$
6	5	an32s	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \to (x \leq y \leftrightarrow \neg y < x)$
7	6	rexbidva	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A x \leq y \leftrightarrow \exists y \in A \neg y < x)$
8		rexnal	$⊢ \exists y \in A \neg y < x \leftrightarrow \neg \forall y \in A y < x$
9	7 8	bitr2di	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\neg \forall y \in A y < x \leftrightarrow \exists y \in A x \leq y)$
10	9	ralbidva	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \neg \forall y \in A y < x \leftrightarrow \forall x \in ℝ \exists y \in A x \leq y)$
11	1 10	bitr3id	$⊢ A \subseteq ℝ^{*} \to (\neg \exists x \in ℝ \forall y \in A y < x \leftrightarrow \forall x \in ℝ \exists y \in A x \leq y)$
12		supxrunb1	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x \leq y \leftrightarrow sup (A ℝ^{} <) = +∞)$
13		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
14		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
15	13 14	syl	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{*} <) < +∞)$
16	11 12 15	3bitrd	$⊢ A \subseteq ℝ^{} \to (\neg \exists x \in ℝ \forall y \in A y < x \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
17	16	con4bid	$⊢ A \subseteq ℝ^{} \to (\exists x \in ℝ \forall y \in A y < x \leftrightarrow sup (A ℝ^{} <) < +∞)$