Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of a subset is equivalent to the complement of the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clsnei.o | |
|
clsnei.p | |
||
clsnei.d | |
||
clsnei.f | |
||
clsnei.h | |
||
clsnei.r | |
||
clsneiel.x | |
||
clsneiel.s | |
||
Assertion | clsneiel1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clsnei.o | |
|
2 | clsnei.p | |
|
3 | clsnei.d | |
|
4 | clsnei.f | |
|
5 | clsnei.h | |
|
6 | clsnei.r | |
|
7 | clsneiel.x | |
|
8 | clsneiel.s | |
|
9 | 3 5 6 | clsneibex | |
10 | 9 | ancli | |
11 | simpr | |
|
12 | 11 | pwexd | |
13 | 1 12 11 4 | fsovfd | |
14 | 13 | ffnd | |
15 | 2 3 11 | dssmapf1od | |
16 | f1of | |
|
17 | 15 16 | syl | |
18 | 5 | breqi | |
19 | 6 18 | sylib | |
20 | 19 | adantr | |
21 | 14 17 20 | brcoffn | |
22 | simprl | |
|
23 | 7 | ad2antrr | |
24 | 8 | ad2antrr | |
25 | 2 3 22 23 24 | ntrclselnel1 | |
26 | simprr | |
|
27 | simplr | |
|
28 | difssd | |
|
29 | 27 28 | sselpwd | |
30 | 1 4 26 23 29 | ntrneiel | |
31 | 30 | notbid | |
32 | 25 31 | bitrd | |
33 | 10 21 32 | syl2anc2 | |