Metamath Proof Explorer

Theorem suprlub

Description: The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)

		Ref	Expression
	Assertion	suprlub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in ℝ) \to (B < sup (A ℝ <) \leftrightarrow \exists z \in A B < z)$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2	1	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to < Or ℝ$
3		sup3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists w \in A y < w))$
4		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to A \subseteq ℝ$
5	2 3 4	suplub2	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in ℝ) \to (B < sup (A ℝ <) \leftrightarrow \exists w \in A B < w)$
6		breq2	$⊢ w = z \to (B < w \leftrightarrow B < z)$
7	6	cbvrexvw	$⊢ \exists w \in A B < w \leftrightarrow \exists z \in A B < z$
8	5 7	bitrdi	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in ℝ) \to (B < sup (A ℝ <) \leftrightarrow \exists z \in A B < z)$