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

Metamath Proof Explorer

Theorem suprubii

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-Sep-1999)

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

Step	Hyp	Ref	Expression
1		sup3i.1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
2		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 ℝ <)$
3	1 2	mpan	$⊢ B \in A \to B \leq sup (A ℝ <)$