Metamath Proof Explorer


Theorem clsneiel1

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 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
clsneiel.x φXB
clsneiel.s φS𝒫B
Assertion clsneiel1 φXKS¬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 clsneiel.x φXB
8 clsneiel.s φS𝒫B
9 3 5 6 clsneibex φBV
10 9 ancli φφBV
11 simpr φBVBV
12 11 pwexd φBV𝒫BV
13 1 12 11 4 fsovfd φBVF:𝒫B𝒫B𝒫𝒫BB
14 13 ffnd φBVFFn𝒫B𝒫B
15 2 3 11 dssmapf1od φBVD:𝒫B𝒫B1-1 onto𝒫B𝒫B
16 f1of D:𝒫B𝒫B1-1 onto𝒫B𝒫BD:𝒫B𝒫B𝒫B𝒫B
17 15 16 syl φBVD:𝒫B𝒫B𝒫B𝒫B
18 5 breqi KHNKFDN
19 6 18 sylib φKFDN
20 19 adantr φBVKFDN
21 14 17 20 brcoffn φBVKDDKDKFN
22 simprl φBVKDDKDKFNKDDK
23 7 ad2antrr φBVKDDKDKFNXB
24 8 ad2antrr φBVKDDKDKFNS𝒫B
25 2 3 22 23 24 ntrclselnel1 φBVKDDKDKFNXKS¬XDKBS
26 simprr φBVKDDKDKFNDKFN
27 simplr φBVKDDKDKFNBV
28 difssd φBVKDDKDKFNBSB
29 27 28 sselpwd φBVKDDKDKFNBS𝒫B
30 1 4 26 23 29 ntrneiel φBVKDDKDKFNXDKBSBSNX
31 30 notbid φBVKDDKDKFN¬XDKBS¬BSNX
32 25 31 bitrd φBVKDDKDKFNXKS¬BSNX
33 10 21 32 syl2anc2 φXKS¬BSNX