Metamath Proof Explorer

Theorem supxrleub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006) (Revised by Mario Carneiro, 6-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		supxrlub	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (B < sup (A ℝ^{*} <) \leftrightarrow \exists x \in A B < x)$
2	1	notbid	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\neg B < sup (A ℝ^{*} <) \leftrightarrow \neg \exists x \in A B < x)$
3		ralnex	$⊢ \forall x \in A \neg B < x \leftrightarrow \neg \exists x \in A B < x$
4	2 3	bitr4di	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\neg B < sup (A ℝ^{*} <) \leftrightarrow \forall x \in A \neg B < x)$
5		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
6		xrlenlt	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land B \in ℝ^{}) \to (sup (A ℝ^{} <) \leq B \leftrightarrow \neg B < sup (A ℝ^{*} <))$
7	5 6	sylan	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (sup (A ℝ^{} <) \leq B \leftrightarrow \neg B < sup (A ℝ^{} <))$
8		simpl	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to A \subseteq ℝ^{*}$
9	8	sselda	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land x \in A) \to x \in ℝ^{*}$
10		simplr	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land x \in A) \to B \in ℝ^{*}$
11	9 10	xrlenltd	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land x \in A) \to (x \leq B \leftrightarrow \neg B < x)$
12	11	ralbidva	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in A x \leq B \leftrightarrow \forall x \in A \neg B < x)$
13	4 7 12	3bitr4d	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (sup (A ℝ^{*} <) \leq B \leftrightarrow \forall x \in A x \leq B)$