neicvgel1

Description: A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of 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	neicvgel1	\|- ( ph -> ( S e. ( N ` X ) <-> -. ( B \ 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	neicvgbex	\|- ( ph -> B e. _V )
11		simpr	\|- ( ( ph /\ B e. _V ) -> B e. _V )
12	11	pwexd	\|- ( ( ph /\ B e. _V ) -> ~P B e. _V )
13	1 12 11 4	fsovf1od	\|- ( ( ph /\ B e. _V ) -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
14		f1ofn	\|- ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> F Fn ( ~P B ^m ~P B ) )
15	13 14	syl	\|- ( ( ph /\ B e. _V ) -> F Fn ( ~P B ^m ~P B ) )
16	2 3 11	dssmapf1od	\|- ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
17		f1of	\|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) )
18	16 17	syl	\|- ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) )
19	1 11 12 5	fsovfd	\|- ( ( ph /\ B e. _V ) -> G : ( ~P ~P B ^m B ) --> ( ~P B ^m ~P B ) )
20	6	breqi	\|- ( N H M <-> N ( F o. ( D o. G ) ) M )
21	7 20	sylib	\|- ( ph -> N ( F o. ( D o. G ) ) M )
22	21	adantr	\|- ( ( ph /\ B e. _V ) -> N ( F o. ( D o. G ) ) M )
23	15 18 19 22	brcofffn	\|- ( ( ph /\ B e. _V ) -> ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) )
24	10 23	mpdan	\|- ( ph -> ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) )
25		simpr2	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( G ` N ) D ( D ` ( G ` N ) ) )
26	8	adantr	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> X e. B )
27	9	adantr	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> S e. ~P B )
28	2 3 25 26 27	ntrclselnel1	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( X e. ( ( G ` N ) ` S ) <-> -. X e. ( ( D ` ( G ` N ) ) ` ( B \ S ) ) ) )
29		eqid	\|- ( ~P B O B ) = ( ~P B O B )
30		simpr1	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> N G ( G ` N ) )
31	5	breqi	\|- ( N G ( G ` N ) <-> N ( B O ~P B ) ( G ` N ) )
32	31	a1i	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( N G ( G ` N ) <-> N ( B O ~P B ) ( G ` N ) ) )
33	10	adantr	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> B e. _V )
34		id	\|- ( B e. _V -> B e. _V )
35		pwexg	\|- ( B e. _V -> ~P B e. _V )
36		eqid	\|- ( B O ~P B ) = ( B O ~P B )
37	1 34 35 36	fsovf1od	\|- ( B e. _V -> ( B O ~P B ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) )
38	33 37	syl	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( B O ~P B ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) )
39		f1orel	\|- ( ( B O ~P B ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) -> Rel ( B O ~P B ) )
40		relbrcnvg	\|- ( Rel ( B O ~P B ) -> ( ( G ` N ) `' ( B O ~P B ) N <-> N ( B O ~P B ) ( G ` N ) ) )
41	38 39 40	3syl	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( ( G ` N ) `' ( B O ~P B ) N <-> N ( B O ~P B ) ( G ` N ) ) )
42	1 34 35 36 29	fsovcnvd	\|- ( B e. _V -> `' ( B O ~P B ) = ( ~P B O B ) )
43	42	breqd	\|- ( B e. _V -> ( ( G ` N ) `' ( B O ~P B ) N <-> ( G ` N ) ( ~P B O B ) N ) )
44	33 43	syl	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( ( G ` N ) `' ( B O ~P B ) N <-> ( G ` N ) ( ~P B O B ) N ) )
45	32 41 44	3bitr2d	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( N G ( G ` N ) <-> ( G ` N ) ( ~P B O B ) N ) )
46	30 45	mpbid	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( G ` N ) ( ~P B O B ) N )
47	1 29 46 26 27	ntrneiel	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( X e. ( ( G ` N ) ` S ) <-> S e. ( N ` X ) ) )
48		simpr3	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( D ` ( G ` N ) ) F M )
49		difssd	\|- ( ph -> ( B \ S ) C_ B )
50	10 49	sselpwd	\|- ( ph -> ( B \ S ) e. ~P B )
51	50	adantr	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( B \ S ) e. ~P B )
52	1 4 48 26 51	ntrneiel	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( X e. ( ( D ` ( G ` N ) ) ` ( B \ S ) ) <-> ( B \ S ) e. ( M ` X ) ) )
53	52	notbid	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( -. X e. ( ( D ` ( G ` N ) ) ` ( B \ S ) ) <-> -. ( B \ S ) e. ( M ` X ) ) )
54	28 47 53	3bitr3d	\|- ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( S e. ( N ` X ) <-> -. ( B \ S ) e. ( M ` X ) ) )
55	24 54	mpdan	\|- ( ph -> ( S e. ( N ` X ) <-> -. ( B \ S ) e. ( M ` X ) ) )

Metamath Proof Explorer

Theorem neicvgel1

Proof