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 \circ D$
		clsneibex.r	$⊢ φ \to K H N$
	Assertion	clsneibex	$⊢ φ \to B \in V$

Proof

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