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\left(B\right)$$
	clsneibex.h	$$⊢H=F\circ D$$
	clsneibex.r	$$⊢\phi \to KHN$$
Assertion	clsneibex	$$⊢\phi \to B\in \mathrm{V}$$

Proof

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