Description: A set A is clopen iff for every point x in the space there is a neighborhood y of x which is either disjoint from A or contained in A . (Contributed by Mario Carneiro, 7-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isclo.1 | |
|
Assertion | isclo2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isclo.1 | |
|
2 | 1 | isclo | |
3 | eleq1w | |
|
4 | 3 | bibi2d | |
5 | 4 | cbvralvw | |
6 | 5 | anbi2i | |
7 | pm4.24 | |
|
8 | raaanv | |
|
9 | 6 7 8 | 3bitr4i | |
10 | bibi1 | |
|
11 | 10 | biimpa | |
12 | 11 | biimpcd | |
13 | 12 | ralimdv | |
14 | 13 | com12 | |
15 | dfss3 | |
|
16 | 14 15 | syl6ibr | |
17 | 16 | ralimi | |
18 | 9 17 | sylbi | |
19 | eleq1w | |
|
20 | 19 | imbi1d | |
21 | 20 | rspcv | |
22 | dfss3 | |
|
23 | 22 | imbi2i | |
24 | r19.21v | |
|
25 | 23 24 | bitr4i | |
26 | 21 25 | imbitrdi | |
27 | ssel | |
|
28 | 27 | com12 | |
29 | 28 | imim2d | |
30 | 29 | ralimdv | |
31 | 26 30 | jcad | |
32 | ralbiim | |
|
33 | 31 32 | syl6ibr | |
34 | 18 33 | impbid2 | |
35 | 34 | pm5.32i | |
36 | 35 | rexbii | |
37 | 36 | ralbii | |
38 | 2 37 | bitrdi | |