Theorem ubioo

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

	Ref	Expression
Assertion	ubioo	|- -. B e. ( A (,) B )

Proof

Step	Hyp	Ref	Expression
1		elioo3g	|- ( B e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ B e. RR* ) /\ ( A < B /\ B < B ) ) )
2	1	simprbi	|- ( B e. ( A (,) B ) -> ( A < B /\ B < B ) )
3	2	simprd	|- ( B e. ( A (,) B ) -> B < B )
4	1	simplbi	|- ( B e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ B e. RR* ) )
5	4	simp2d	|- ( B e. ( A (,) B ) -> B e. RR* )
6		xrltnr	|- ( B e. RR* -> -. B < B )
7	5 6	syl	|- ( B e. ( A (,) B ) -> -. B < B )
8	3 7	pm2.65i	|- -. B e. ( A (,) B )