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	ffvelrnd	|- ( 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 ) } )