Theorem ubioo

Description: An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Assertion	ubioo	$$⊢\neg B\in \left(A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elioo3g	$$⊢B\in \left(A,B\right)\leftrightarrow \left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \left(A<B\wedge B<B\right)\right)$$
2	1	simprbi	$$⊢B\in \left(A,B\right)\to \left(A<B\wedge B<B\right)$$
3	2	simprd	$$⊢B\in \left(A,B\right)\to B<B$$
4	1	simplbi	$$⊢B\in \left(A,B\right)\to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
5	4	simp2d	$$⊢B\in \left(A,B\right)\to B\in {ℝ}^{*}$$
6		xrltnr	$$⊢B\in {ℝ}^{*}\to \neg B<B$$
7	5 6	syl	$$⊢B\in \left(A,B\right)\to \neg B<B$$
8	3 7	pm2.65i	$$⊢\neg B\in \left(A,B\right)$$