Description: Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clsnei.o | |
|
clsnei.p | |
||
clsnei.d | |
||
clsnei.f | |
||
clsnei.h | |
||
clsnei.r | |
||
clsneifv.s | |
||
Assertion | clsneifv4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clsnei.o | |
|
2 | clsnei.p | |
|
3 | clsnei.d | |
|
4 | clsnei.f | |
|
5 | clsnei.h | |
|
6 | clsnei.r | |
|
7 | clsneifv.s | |
|
8 | dfin5 | |
|
9 | 1 2 3 4 5 6 | clsneikex | |
10 | elmapi | |
|
11 | 9 10 | syl | |
12 | 11 7 | ffvelrnd | |
13 | 12 | elpwid | |
14 | sseqin2 | |
|
15 | 13 14 | sylib | |
16 | 6 | adantr | |
17 | simpr | |
|
18 | 7 | adantr | |
19 | 1 2 3 4 5 16 17 18 | clsneiel1 | |
20 | 19 | rabbidva | |
21 | 8 15 20 | 3eqtr3a | |