Metamath Proof Explorer

Theorem lbioc

Description: A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
2 1 elixx3g 
 |-  ( A e. ( A (,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ A e. RR* ) /\ ( A < A /\ A <_ B ) ) )
3 2 biimpi 
 |-  ( A e. ( A (,] B ) -> ( ( A e. RR* /\ B e. RR* /\ A e. RR* ) /\ ( A < A /\ A <_ B ) ) )
4 3 simprld 
 |-  ( A e. ( A (,] B ) -> A < A )
5 1 elmpocl1 
 |-  ( 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 4 7 pm2.65i 
 |-  -. A e. ( A (,] B )