Metamath Proof Explorer

Theorem clsneiel1

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of a subset is equivalent to the complement of 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 clsneiel1 
|- ( ph -> ( X e. ( K ` S ) <-> -. ( B \ 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 clsneibex 
 |-  ( ph -> B e. _V )
10 9 ancli 
 |-  ( ph -> ( 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 fsovfd 
 |-  ( ( ph /\ B e. _V ) -> F : ( ~P B ^m ~P B ) --> ( ~P ~P B ^m B ) )
14 13 ffnd 
 |-  ( ( ph /\ B e. _V ) -> F Fn ( ~P B ^m ~P B ) )
15 2 3 11 dssmapf1od 
 |-  ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
16 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 ) )
17 15 16 syl 
 |-  ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) )
18 5 breqi 
 |-  ( K H N <-> K ( F o. D ) N )
19 6 18 sylib 
 |-  ( ph -> K ( F o. D ) N )
20 19 adantr 
 |-  ( ( ph /\ B e. _V ) -> K ( F o. D ) N )
21 14 17 20 brcoffn 
 |-  ( ( ph /\ B e. _V ) -> ( K D ( D ` K ) /\ ( D ` K ) F N ) )
22 simprl 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> K D ( D ` K ) )
23 7 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> X e. B )
24 8 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> S e. ~P B )
25 2 3 22 23 24 ntrclselnel1 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( X e. ( K ` S ) <-> -. X e. ( ( D ` K ) ` ( B \ S ) ) ) )
26 simprr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( D ` K ) F N )
27 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> B e. _V )
28 difssd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( B \ S ) C_ B )
29 27 28 sselpwd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( B \ S ) e. ~P B )
30 1 4 26 23 29 ntrneiel 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( X e. ( ( D ` K ) ` ( B \ S ) ) <-> ( B \ S ) e. ( N ` X ) ) )
31 30 notbid 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( -. X e. ( ( D ` K ) ` ( B \ S ) ) <-> -. ( B \ S ) e. ( N ` X ) ) )
32 25 31 bitrd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( K D ( D ` K ) /\ ( D ` K ) F N ) ) -> ( X e. ( K ` S ) <-> -. ( B \ S ) e. ( N ` X ) ) )
33 10 21 32 syl2anc2 
 |-  ( ph -> ( X e. ( K ` S ) <-> -. ( B \ S ) e. ( N ` X ) ) )