suprub

Description: A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004)

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

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to A \subseteq ℝ$
2	1	sselda	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in A) \to B \in ℝ$
3		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
4	3	adantr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in A) \to sup (A ℝ <) \in ℝ$
5		ltso	$⊢ < Or ℝ$
6	5	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to < Or ℝ$
7		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 z \in A y < z))$
8	6 7	supub	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (B \in A \to \neg sup (A ℝ <) < B)$
9	8	imp	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in A) \to \neg sup (A ℝ <) < B$
10	2 4 9	nltled	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land B \in A) \to B \leq sup (A ℝ <)$

Metamath Proof Explorer