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 ) |
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 ) |