Theorem neicvgel2

Description: The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		neicvg.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		neicvg.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3		neicvg.d	|- D = ( P ` B )
4		neicvg.f	|- F = ( ~P B O B )
5		neicvg.g	|- G = ( B O ~P B )
6		neicvg.h	|- H = ( F o. ( D o. G ) )
7		neicvg.r	|- ( ph -> N H M )
8		neicvgel.x	|- ( ph -> X e. B )
9		neicvgel.s	|- ( ph -> S e. ~P B )
10	3 6 7	neicvgrcomplex	|- ( ph -> ( B \ S ) e. ~P B )
11	1 2 3 4 5 6 7 8 10	neicvgel1	|- ( ph -> ( ( B \ S ) e. ( N ` X ) <-> -. ( B \ ( B \ S ) ) e. ( M ` X ) ) )
12	9	elpwid	|- ( ph -> S C_ B )
13		dfss4	|- ( S C_ B <-> ( B \ ( B \ S ) ) = S )
14	12 13	sylib	|- ( ph -> ( B \ ( B \ S ) ) = S )
15	14	eleq1d	|- ( ph -> ( ( B \ ( B \ S ) ) e. ( M ` X ) <-> S e. ( M ` X ) ) )
16	15	notbid	|- ( ph -> ( -. ( B \ ( B \ S ) ) e. ( M ` X ) <-> -. S e. ( M ` X ) ) )
17	11 16	bitrd	|- ( ph -> ( ( B \ S ) e. ( N ` X ) <-> -. S e. ( M ` X ) ) )