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

Metamath Proof Explorer

Theorem supxrlub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Assertion	supxrlub	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (B < sup (A ℝ^{*} <) \leftrightarrow \exists x \in A B < x)$

Step	Hyp	Ref	Expression
1		xrltso	$⊢ < Or ℝ^{*}$
2	1	a1i	$⊢ A \subseteq ℝ^{} \to < Or ℝ^{}$
3		xrsupss	$⊢ A \subseteq ℝ^{} \to \exists y \in ℝ^{} (\forall z \in A \neg y < z \land \forall z \in ℝ^{*} (z < y \to \exists x \in A z < x))$
4		id	$⊢ A \subseteq ℝ^{} \to A \subseteq ℝ^{}$
5	2 3 4	suplub2	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (B < sup (A ℝ^{*} <) \leftrightarrow \exists x \in A B < x)$