Theorem ntrneifv4

Description: The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
	ntrnei.f	|- F = ( ~P B O B )
	ntrnei.r	|- ( ph -> I F N )
	ntrneifv.s	|- ( ph -> S e. ~P B )
Assertion	ntrneifv4	|- ( ph -> ( I ` S ) = { x e. B | S e. ( N ` x ) } )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.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		ntrnei.f	|- F = ( ~P B O B )
3		ntrnei.r	|- ( ph -> I F N )
4		ntrneifv.s	|- ( ph -> S e. ~P B )
5		dfin5	|- ( B i^i ( I ` S ) ) = { x e. B | x e. ( I ` S ) }
6	1 2 3	ntrneiiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
7		elmapi	|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
8	6 7	syl	|- ( ph -> I : ~P B --> ~P B )
9	8 4	ffvelcdmd	|- ( ph -> ( I ` S ) e. ~P B )
10	9	elpwid	|- ( ph -> ( I ` S ) C_ B )
11		sseqin2	|- ( ( I ` S ) C_ B <-> ( B i^i ( I ` S ) ) = ( I ` S ) )
12	10 11	sylib	|- ( ph -> ( B i^i ( I ` S ) ) = ( I ` S ) )
13	3	adantr	|- ( ( ph /\ x e. B ) -> I F N )
14		simpr	|- ( ( ph /\ x e. B ) -> x e. B )
15	4	adantr	|- ( ( ph /\ x e. B ) -> S e. ~P B )
16	1 2 13 14 15	ntrneiel	|- ( ( ph /\ x e. B ) -> ( x e. ( I ` S ) <-> S e. ( N ` x ) ) )
17	16	rabbidva	|- ( ph -> { x e. B | x e. ( I ` S ) } = { x e. B | S e. ( N ` x ) } )
18	5 12 17	3eqtr3a	|- ( ph -> ( I ` S ) = { x e. B | S e. ( N ` x ) } )