supxr2

Description: The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006)

		Ref	Expression
	Assertion	supxr2	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land (\forall x \in A x \leq B \land \forall x \in ℝ (x < B \to \exists y \in A x < y))) \to sup (A ℝ^{*} <) = B$

Step	Hyp	Ref	Expression
1		ssel2	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \in ℝ^{}$
2		xrlenlt	$⊢ (x \in ℝ^{} \land B \in ℝ^{}) \to (x \leq B \leftrightarrow \neg B < x)$
3	1 2	sylan	$⊢ ((A \subseteq ℝ^{} \land x \in A) \land B \in ℝ^{}) \to (x \leq B \leftrightarrow \neg B < x)$
4	3	an32s	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land x \in A) \to (x \leq B \leftrightarrow \neg B < x)$
5	4	ralbidva	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in A x \leq B \leftrightarrow \forall x \in A \neg B < x)$
6	5	anbi1d	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to ((\forall x \in A x \leq B \land \forall x \in ℝ (x < B \to \exists y \in A x < y)) \leftrightarrow (\forall x \in A \neg B < x \land \forall x \in ℝ (x < B \to \exists y \in A x < y)))$
7	6	biimpa	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land (\forall x \in A x \leq B \land \forall x \in ℝ (x < B \to \exists y \in A x < y))) \to (\forall x \in A \neg B < x \land \forall x \in ℝ (x < B \to \exists y \in A x < y))$
8		supxr	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land (\forall x \in A \neg B < x \land \forall x \in ℝ (x < B \to \exists y \in A x < y))) \to sup (A ℝ^{*} <) = B$
9	7 8	syldan	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land (\forall x \in A x \leq B \land \forall x \in ℝ (x < B \to \exists y \in A x < y))) \to sup (A ℝ^{*} <) = B$

Metamath Proof Explorer