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 = i V , j V k 𝒫 j i l j m i | l k m
clsnei.p P = n V p 𝒫 n 𝒫 n o 𝒫 n n p n o
clsnei.d D = P B
clsnei.f F = 𝒫 B O B
clsnei.h H = F D
clsnei.r φ K H N
Assertion clsneikex φ K 𝒫 B 𝒫 B

Proof

Step Hyp Ref Expression
1 clsnei.o O = i V , j V k 𝒫 j i l j m i | l k m
2 clsnei.p P = n V p 𝒫 n 𝒫 n o 𝒫 n n p n o
3 clsnei.d D = P B
4 clsnei.f F = 𝒫 B O B
5 clsnei.h H = F D
6 clsnei.r φ K H N
7 3 5 6 clsneibex φ B V
8 pwexg B V 𝒫 B V
9 8 adantl φ B V 𝒫 B V
10 simpr φ B V B V
11 1 9 10 4 fsovf1od φ B V F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B
12 f1ofn F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B F Fn 𝒫 B 𝒫 B
13 11 12 syl φ B V F Fn 𝒫 B 𝒫 B
14 2 3 10 dssmapf1od φ B V D : 𝒫 B 𝒫 B 1-1 onto 𝒫 B 𝒫 B
15 f1of D : 𝒫 B 𝒫 B 1-1 onto 𝒫 B 𝒫 B D : 𝒫 B 𝒫 B 𝒫 B 𝒫 B
16 14 15 syl φ B V D : 𝒫 B 𝒫 B 𝒫 B 𝒫 B
17 6 adantr φ B V K H N
18 5 breqi K H N K F D N
19 17 18 sylib φ B V K F D N
20 13 16 19 brcoffn φ B V K D D K D K F N
21 7 20 mpdan φ K D D K D K F N
22 21 simpld φ K D D K
23 2 3 22 ntrclsiex φ K 𝒫 B 𝒫 B