Metamath Proof Explorer


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 )