Metamath Proof Explorer


Theorem clsneifv4

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 O=iV,jVk𝒫jiljmi|lkm
clsnei.p P=nVp𝒫n𝒫no𝒫nnpno
clsnei.d D=PB
clsnei.f F=𝒫BOB
clsnei.h H=FD
clsnei.r φKHN
clsneifv.s φS𝒫B
Assertion clsneifv4 φKS=xB|¬BSNx

Proof

Step Hyp Ref Expression
1 clsnei.o O=iV,jVk𝒫jiljmi|lkm
2 clsnei.p P=nVp𝒫n𝒫no𝒫nnpno
3 clsnei.d D=PB
4 clsnei.f F=𝒫BOB
5 clsnei.h H=FD
6 clsnei.r φKHN
7 clsneifv.s φS𝒫B
8 dfin5 BKS=xB|xKS
9 1 2 3 4 5 6 clsneikex φK𝒫B𝒫B
10 elmapi K𝒫B𝒫BK:𝒫B𝒫B
11 9 10 syl φK:𝒫B𝒫B
12 11 7 ffvelrnd φKS𝒫B
13 12 elpwid φKSB
14 sseqin2 KSBBKS=KS
15 13 14 sylib φBKS=KS
16 6 adantr φxBKHN
17 simpr φxBxB
18 7 adantr φxBS𝒫B
19 1 2 3 4 5 16 17 18 clsneiel1 φxBxKS¬BSNx
20 19 rabbidva φxB|xKS=xB|¬BSNx
21 8 15 20 3eqtr3a φKS=xB|¬BSNx