Theorem lbioo

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

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

Proof

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