Theorem clsneiel2

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021)

	Ref	Expression
Hypotheses	clsnei.o	|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
	clsnei.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
	clsnei.d	|- D = ( P ` B )
	clsnei.f	|- F = ( ~P B O B )
	clsnei.h	|- H = ( F o. D )
	clsnei.r	|- ( ph -> K H N )
	clsneiel.x	|- ( ph -> X e. B )
	clsneiel.s	|- ( ph -> S e. ~P B )
Assertion	clsneiel2	|- ( ph -> ( X e. ( K ` ( B \ S ) ) <-> -. S e. ( N ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		clsnei.o	|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2		clsnei.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3		clsnei.d	|- D = ( P ` B )
4		clsnei.f	|- F = ( ~P B O B )
5		clsnei.h	|- H = ( F o. D )
6		clsnei.r	|- ( ph -> K H N )
7		clsneiel.x	|- ( ph -> X e. B )
8		clsneiel.s	|- ( ph -> S e. ~P B )
9	3 5 6	clsneircomplex	|- ( ph -> ( B \ S ) e. ~P B )
10	1 2 3 4 5 6 7 9	clsneiel1	|- ( ph -> ( X e. ( K ` ( B \ S ) ) <-> -. ( B \ ( B \ S ) ) e. ( N ` X ) ) )
11	8	elpwid	|- ( ph -> S C_ B )
12		dfss4	|- ( S C_ B <-> ( B \ ( B \ S ) ) = S )
13	11 12	sylib	|- ( ph -> ( B \ ( B \ S ) ) = S )
14	13	eleq1d	|- ( ph -> ( ( B \ ( B \ S ) ) e. ( N ` X ) <-> S e. ( N ` X ) ) )
15	14	notbid	|- ( ph -> ( -. ( B \ ( B \ S ) ) e. ( N ` X ) <-> -. S e. ( N ` X ) ) )
16	10 15	bitrd	|- ( ph -> ( X e. ( K ` ( B \ S ) ) <-> -. S e. ( N ` X ) ) )