Description: An open interval with identical lower and upper bounds is empty. (Contributed by NM, 21-Jun-2007) (Revised by Mario Carneiro, 3-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | iooid | |- ( A (,) A ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xrleid | |- ( A e. RR* -> A <_ A ) |
|
| 2 | 1 | adantr | |- ( ( A e. RR* /\ A e. RR* ) -> A <_ A ) |
| 3 | ioo0 | |- ( ( A e. RR* /\ A e. RR* ) -> ( ( A (,) A ) = (/) <-> A <_ A ) ) |
|
| 4 | 2 3 | mpbird | |- ( ( A e. RR* /\ A e. RR* ) -> ( A (,) A ) = (/) ) |
| 5 | ndmioo | |- ( -. ( A e. RR* /\ A e. RR* ) -> ( A (,) A ) = (/) ) |
|
| 6 | 4 5 | pm2.61i | |- ( A (,) A ) = (/) |