Metamath Proof Explorer


Theorem clsneibex

Description: If (pseudo-)closure and (pseudo-)neighborhood functions are related by the composite operator, H , then the base set exists. (Contributed by RP, 4-Jun-2021)

Ref Expression
Hypotheses clsneibex.d D = P B
clsneibex.h H = F D
clsneibex.r φ K H N
Assertion clsneibex φ B V

Proof

Step Hyp Ref Expression
1 clsneibex.d D = P B
2 clsneibex.h H = F D
3 clsneibex.r φ K H N
4 1 coeq2i F D = F P B
5 2 4 eqtri H = F P B
6 5 a1i φ H = F P B
7 6 3 breqdi φ K F P B N
8 brne0 K F P B N F P B
9 fvprc ¬ B V P B =
10 9 rneqd ¬ B V ran P B = ran
11 rn0 ran =
12 10 11 eqtrdi ¬ B V ran P B =
13 12 ineq2d ¬ B V dom F ran P B = dom F
14 in0 dom F =
15 13 14 eqtrdi ¬ B V dom F ran P B =
16 15 coemptyd ¬ B V F P B =
17 16 necon1ai F P B B V
18 7 8 17 3syl φ B V