Metamath Proof Explorer

Theorem clsneifv3

Description: Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-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 )
clsneifv.x 
|- ( ph -> X e. B )
Assertion clsneifv3 
|- ( ph -> ( N ` X ) = { s e. ~P B | -. X e. ( K ` ( B \ s ) ) } )

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 clsneifv.x 
 |-  ( ph -> X e. B )
8 dfin5 
 |-  ( ~P B i^i ( N ` X ) ) = { s e. ~P B | s e. ( N ` X ) }
9 1 2 3 4 5 6 clsneinex 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
10 elmapi 
 |-  ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
11 9 10 syl 
 |-  ( ph -> N : B --> ~P ~P B )
12 11 7 ffvelrnd 
 |-  ( ph -> ( N ` X ) e. ~P ~P B )
13 12 elpwid 
 |-  ( ph -> ( N ` X ) C_ ~P B )
14 sseqin2 
 |-  ( ( N ` X ) C_ ~P B <-> ( ~P B i^i ( N ` X ) ) = ( N ` X ) )
15 13 14 sylib 
 |-  ( ph -> ( ~P B i^i ( N ` X ) ) = ( N ` X ) )
16 6 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> K H N )
17 7 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> X e. B )
18 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
19 1 2 3 4 5 16 17 18 clsneiel2 
 |-  ( ( ph /\ s e. ~P B ) -> ( X e. ( K ` ( B \ s ) ) <-> -. s e. ( N ` X ) ) )
20 19 con2bid 
 |-  ( ( ph /\ s e. ~P B ) -> ( s e. ( N ` X ) <-> -. X e. ( K ` ( B \ s ) ) ) )
21 20 rabbidva 
 |-  ( ph -> { s e. ~P B | s e. ( N ` X ) } = { s e. ~P B | -. X e. ( K ` ( B \ s ) ) } )
22 8 15 21 3eqtr3a 
 |-  ( ph -> ( N ` X ) = { s e. ~P B | -. X e. ( K ` ( B \ s ) ) } )