Metamath Proof Explorer

Theorem clsneifv4

Description: Value of the closure (interior) function in terms of the neighborhoods (convergents) 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.s 
|- ( ph -> S e. ~P B )
Assertion clsneifv4 
|- ( ph -> ( K ` S ) = { x e. B | -. ( 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 clsneifv.s 
 |-  ( ph -> S e. ~P B )
8 dfin5 
 |-  ( B i^i ( K ` S ) ) = { x e. B | x e. ( K ` S ) }
9 1 2 3 4 5 6 clsneikex 
 |-  ( ph -> K e. ( ~P B ^m ~P B ) )
10 elmapi 
 |-  ( K e. ( ~P B ^m ~P B ) -> K : ~P B --> ~P B )
11 9 10 syl 
 |-  ( ph -> K : ~P B --> ~P B )
12 11 7 ffvelcdmd 
 |-  ( ph -> ( K ` S ) e. ~P B )
13 12 elpwid 
 |-  ( ph -> ( K ` S ) C_ B )
14 sseqin2 
 |-  ( ( K ` S ) C_ B <-> ( B i^i ( K ` S ) ) = ( K ` S ) )
15 13 14 sylib 
 |-  ( ph -> ( B i^i ( K ` S ) ) = ( K ` S ) )
16 6 adantr 
 |-  ( ( ph /\ x e. B ) -> K H N )
17 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
18 7 adantr 
 |-  ( ( ph /\ x e. B ) -> S e. ~P B )
19 1 2 3 4 5 16 17 18 clsneiel1 
 |-  ( ( ph /\ x e. B ) -> ( x e. ( K ` S ) <-> -. ( B \ S ) e. ( N ` x ) ) )
20 19 rabbidva 
 |-  ( ph -> { x e. B | x e. ( K ` S ) } = { x e. B | -. ( B \ S ) e. ( N ` x ) } )
21 8 15 20 3eqtr3a 
 |-  ( ph -> ( K ` S ) = { x e. B | -. ( B \ S ) e. ( N ` x ) } )