Metamath Proof Explorer

Theorem 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 f1orel 
 |-  ( ( B O ~P B ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) -> Rel ( B O ~P B ) )
39 relbrcnvg 
 |-  ( Rel ( B O ~P B ) -> ( ( G ` N ) `' ( B O ~P B ) N <-> N ( B O ~P B ) ( G ` N ) ) )
40 33 37 38 39 4syl 
 |-  ( ( 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 ) ) )
41 1 34 35 36 29 fsovcnvd 
 |-  ( B e. _V -> `' ( B O ~P B ) = ( ~P B O B ) )
42 41 breqd 
 |-  ( B e. _V -> ( ( G ` N ) `' ( B O ~P B ) N <-> ( G ` N ) ( ~P B O B ) N ) )
43 33 42 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 ) )
44 32 40 43 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 ) )
45 30 44 mpbid 
 |-  ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( G ` N ) ( ~P B O B ) N )
46 1 29 45 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 ) ) )
47 simpr3 
 |-  ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( D ` ( G ` N ) ) F M )
48 difssd 
 |-  ( ph -> ( B \ S ) C_ B )
49 10 48 sselpwd 
 |-  ( ph -> ( B \ S ) e. ~P B )
50 49 adantr 
 |-  ( ( ph /\ ( N G ( G ` N ) /\ ( G ` N ) D ( D ` ( G ` N ) ) /\ ( D ` ( G ` N ) ) F M ) ) -> ( B \ S ) e. ~P B )
51 1 4 47 26 50 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 ) ) )
52 51 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 ) ) )
53 28 46 52 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 ) ) )
54 24 53 mpdan 
 |-  ( ph -> ( S e. ( N ` X ) <-> -. ( B \ S ) e. ( M ` X ) ) )