supxr

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

		Ref	Expression
	Assertion	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$

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((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 B \in ℝ^{*}$
2		simprl	$⊢ ((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 \forall x \in A \neg B < x$
3		xrub	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \leftrightarrow \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y))$
4	3	biimpa	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall x \in ℝ (x < B \to \exists y \in A x < y)) \to \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y)$
5	4	adantrl	$⊢ ((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 \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y)$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	a1i	$⊢ ⊤ \to < Or ℝ^{*}$
8	7	eqsup	$⊢ ⊤ \to ((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	8	mptru	$⊢ (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$
10	1 2 5 9	syl3anc	$⊢ ((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$

Metamath Proof Explorer