ubicc2

Description: The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007) (Revised by FL, 29-May-2014)

		Ref	Expression
	Assertion	ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in ℝ^{*}$
2		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \leq B$
3		xrleid	$⊢ B \in ℝ^{*} \to B \leq B$
4	3	3ad2ant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \leq B$
5		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \in [A, B] \leftrightarrow (B \in ℝ^{*} \land A \leq B \land B \leq B))$
6	5	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (B \in [A, B] \leftrightarrow (B \in ℝ^{*} \land A \leq B \land B \leq B))$
7	1 2 4 6	mpbir3and	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$

Metamath Proof Explorer