Theorem ntrneik4

Description: Idempotence of the interior function is equivalent to stating a set, s , is a neighborhood of a point, x is equivalent to there existing a special neighborhood, u , of x such that a point is an element of the special neighborhood if and only if s is also a neighborhood of the point. (Contributed by RP, 11-Jul-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 )
Assertion	ntrneik4	|- ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) ) )

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	1 2 3	ntrneik4w	|- ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
5	3	ad2antrr	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> I F N )
6		simplr	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> x e. B )
7	1 2 3	ntrneiiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
8		elmapi	|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
9	7 8	syl	|- ( ph -> I : ~P B --> ~P B )
10	9	ffvelrnda	|- ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
11	10	adantlr	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
12	1 2 5 6 11	ntrneiel	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> ( x e. ( I ` ( I ` s ) ) <-> ( I ` s ) e. ( N ` x ) ) )
13		simpr	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> s e. ~P B )
14	1 2 5 6 13	ntrneiel2	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> ( x e. ( I ` ( I ` s ) ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) )
15	12 14	bitr3d	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> ( ( I ` s ) e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) )
16	15	bibi2d	|- ( ( ( ph /\ x e. B ) /\ s e. ~P B ) -> ( ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) <-> ( s e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) ) )
17	16	ralbidva	|- ( ( ph /\ x e. B ) -> ( A. s e. ~P B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) <-> A. s e. ~P B ( s e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) ) )
18	17	ralbidva	|- ( ph -> ( A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) ) )
19	4 18	bitrd	|- ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> E. u e. ( N ` x ) A. y e. B ( y e. u <-> s e. ( N ` y ) ) ) ) )