Description: Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clscld.1 | |
|
Assertion | ntreq0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clscld.1 | |
|
2 | 1 | ntrval | |
3 | 2 | eqeq1d | |
4 | neq0 | |
|
5 | 4 | con1bii | |
6 | ancom | |
|
7 | elin | |
|
8 | 7 | anbi1i | |
9 | anass | |
|
10 | 6 8 9 | 3bitri | |
11 | 10 | exbii | |
12 | eluni | |
|
13 | df-rex | |
|
14 | 11 12 13 | 3bitr4i | |
15 | 14 | exbii | |
16 | rexcom4 | |
|
17 | 19.42v | |
|
18 | 17 | rexbii | |
19 | 15 16 18 | 3bitr2i | |
20 | 19 | notbii | |
21 | 5 20 | bitr3i | |
22 | ralinexa | |
|
23 | velpw | |
|
24 | neq0 | |
|
25 | 24 | con1bii | |
26 | 23 25 | imbi12i | |
27 | 26 | ralbii | |
28 | 21 22 27 | 3bitr2i | |
29 | 3 28 | bitrdi | |