Metamath Proof Explorer


Theorem clsneikex

Description: If closure and neighborhoods functions are related, the closure function exists. (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
Assertion clsneikex φK𝒫B𝒫B

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 3 5 6 clsneibex φBV
8 pwexg BV𝒫BV
9 8 adantl φBV𝒫BV
10 simpr φBVBV
11 1 9 10 4 fsovf1od φBVF:𝒫B𝒫B1-1 onto𝒫𝒫BB
12 f1ofn F:𝒫B𝒫B1-1 onto𝒫𝒫BBFFn𝒫B𝒫B
13 11 12 syl φBVFFn𝒫B𝒫B
14 2 3 10 dssmapf1od φBVD:𝒫B𝒫B1-1 onto𝒫B𝒫B
15 f1of D:𝒫B𝒫B1-1 onto𝒫B𝒫BD:𝒫B𝒫B𝒫B𝒫B
16 14 15 syl φBVD:𝒫B𝒫B𝒫B𝒫B
17 6 adantr φBVKHN
18 5 breqi KHNKFDN
19 17 18 sylib φBVKFDN
20 13 16 19 brcoffn φBVKDDKDKFN
21 7 20 mpdan φKDDKDKFN
22 21 simpld φKDDK
23 2 3 22 ntrclsiex φK𝒫B𝒫B