Theorem ntrneifv3

Description: The value of the neighbors (convergents) expressed in terms of the interior (closure) 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 )
	ntrnei.x	|- ( ph -> X e. B )
Assertion	ntrneifv3	|- ( ph -> ( N ` X ) = { s e. ~P B | X e. ( I ` s ) } )

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