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 o. D )
	clsneibex.r	|- ( ph -> K H N )
Assertion	clsneibex	|- ( ph -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		clsneibex.d	|- D = ( P ` B )
2		clsneibex.h	|- H = ( F o. D )
3		clsneibex.r	|- ( ph -> K H N )
4	1	coeq2i	|- ( F o. D ) = ( F o. ( P ` B ) )
5	2 4	eqtri	|- H = ( F o. ( P ` B ) )
6	5	a1i	|- ( ph -> H = ( F o. ( P ` B ) ) )
7	6 3	breqdi	|- ( ph -> K ( F o. ( P ` B ) ) N )
8		brne0	|- ( K ( F o. ( P ` B ) ) N -> ( F o. ( P ` B ) ) =/= (/) )
9		fvprc	|- ( -. B e. _V -> ( P ` B ) = (/) )
10	9	rneqd	|- ( -. B e. _V -> ran ( P ` B ) = ran (/) )
11		rn0	|- ran (/) = (/)
12	10 11	eqtrdi	|- ( -. B e. _V -> ran ( P ` B ) = (/) )
13	12	ineq2d	|- ( -. B e. _V -> ( dom F i^i ran ( P ` B ) ) = ( dom F i^i (/) ) )
14		in0	|- ( dom F i^i (/) ) = (/)
15	13 14	eqtrdi	|- ( -. B e. _V -> ( dom F i^i ran ( P ` B ) ) = (/) )
16	15	coemptyd	|- ( -. B e. _V -> ( F o. ( P ` B ) ) = (/) )
17	16	necon1ai	|- ( ( F o. ( P ` B ) ) =/= (/) -> B e. _V )
18	7 8 17	3syl	|- ( ph -> B e. _V )