Theorem 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	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A\le B\right)\to B\in \left[A,B\right]$$

Proof

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