Metamath Proof Explorer

Theorem ntrneik4w

Description: Idempotence of the interior function is equivalent to saying a set is a neighborhood of a point if and only if the interior of the set is a neighborhood of a 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 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 ) ) ) )

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 dfcleq 
 |-  ( ( I ` s ) = ( I ` ( I ` s ) ) <-> A. x ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) )
5 eqcom 
 |-  ( ( I ` ( I ` s ) ) = ( I ` s ) <-> ( I ` s ) = ( I ` ( I ` s ) ) )
6 ralv 
 |-  ( A. x e. _V ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) <-> A. x ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) )
7 4 5 6 3bitr4i 
 |-  ( ( I ` ( I ` s ) ) = ( I ` s ) <-> A. x e. _V ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) )
8 ssv 
 |-  B C_ _V
9 8 a1i 
 |-  ( ( ph /\ s e. ~P B ) -> B C_ _V )
10 vex 
 |-  x e. _V
11 eldif 
 |-  ( x e. ( _V \ B ) <-> ( x e. _V /\ -. x e. B ) )
12 10 11 mpbiran 
 |-  ( x e. ( _V \ B ) <-> -. x e. B )
13 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
14 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
15 13 14 syl 
 |-  ( ph -> I : ~P B --> ~P B )
16 15 ffvelrnda 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
17 16 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B )
18 17 sseld 
 |-  ( ( ph /\ s e. ~P B ) -> ( x e. ( I ` s ) -> x e. B ) )
19 18 con3dimp 
 |-  ( ( ( ph /\ s e. ~P B ) /\ -. x e. B ) -> -. x e. ( I ` s ) )
20 15 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> I : ~P B --> ~P B )
21 20 16 ffvelrnd 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` ( I ` s ) ) e. ~P B )
22 21 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` ( I ` s ) ) C_ B )
23 22 sseld 
 |-  ( ( ph /\ s e. ~P B ) -> ( x e. ( I ` ( I ` s ) ) -> x e. B ) )
24 23 con3dimp 
 |-  ( ( ( ph /\ s e. ~P B ) /\ -. x e. B ) -> -. x e. ( I ` ( I ` s ) ) )
25 19 24 2falsed 
 |-  ( ( ( ph /\ s e. ~P B ) /\ -. x e. B ) -> ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) )
26 25 ex 
 |-  ( ( ph /\ s e. ~P B ) -> ( -. x e. B -> ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) ) )
27 12 26 syl5bi 
 |-  ( ( ph /\ s e. ~P B ) -> ( x e. ( _V \ B ) -> ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) ) )
28 27 ralrimiv 
 |-  ( ( ph /\ s e. ~P B ) -> A. x e. ( _V \ B ) ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) )
29 9 28 raldifeq 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x e. B ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) <-> A. x e. _V ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) ) )
30 3 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> I F N )
31 30 adantr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> I F N )
32 simpr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> x e. B )
33 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> s e. ~P B )
34 1 2 31 32 33 ntrneiel 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
35 16 adantr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( I ` s ) e. ~P B )
36 1 2 31 32 35 ntrneiel 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( x e. ( I ` ( I ` s ) ) <-> ( I ` s ) e. ( N ` x ) ) )
37 34 36 bibi12d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) <-> ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
38 37 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x e. B ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) <-> A. x e. B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
39 29 38 bitr3d 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x e. _V ( x e. ( I ` s ) <-> x e. ( I ` ( I ` s ) ) ) <-> A. x e. B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
40 7 39 syl5bb 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` ( I ` s ) ) = ( I ` s ) <-> A. x e. B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
41 40 ralbidva 
 |-  ( ph -> ( A. s e. ~P B ( I ` ( I ` s ) ) = ( I ` s ) <-> A. s e. ~P B A. x e. B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) ) )
42 ralcom 
 |-  ( A. s e. ~P B A. x e. B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) <-> ( I ` s ) e. ( N ` x ) ) )
43 41 42 bitrdi 
 |-  ( 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 ) ) ) )