Metamath Proof Explorer

Theorem ntrneix2

Description: An interior (closure) function is expansive if and only if all subsets which contain a point are neighborhoods (convergents) of that point. (Contributed by RP, 11-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 )
Assertion ntrneix2 
|- ( ph -> ( A. s e. ~P B s C_ ( I ` s ) <-> A. x e. B A. s e. ~P B ( x e. s -> 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 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
5 elpwi 
 |-  ( s e. ~P B -> s C_ B )
6 5 sselda 
 |-  ( ( s e. ~P B /\ x e. s ) -> x e. B )
7 biimt 
 |-  ( x e. B -> ( x e. ( I ` s ) <-> ( x e. B -> x e. ( I ` s ) ) ) )
8 6 7 syl 
 |-  ( ( s e. ~P B /\ x e. s ) -> ( x e. ( I ` s ) <-> ( x e. B -> x e. ( I ` s ) ) ) )
9 8 pm5.74da 
 |-  ( s e. ~P B -> ( ( x e. s -> x e. ( I ` s ) ) <-> ( x e. s -> ( x e. B -> x e. ( I ` s ) ) ) ) )
10 bi2.04 
 |-  ( ( x e. s -> ( x e. B -> x e. ( I ` s ) ) ) <-> ( x e. B -> ( x e. s -> x e. ( I ` s ) ) ) )
11 9 10 bitrdi 
 |-  ( s e. ~P B -> ( ( x e. s -> x e. ( I ` s ) ) <-> ( x e. B -> ( x e. s -> x e. ( I ` s ) ) ) ) )
12 11 albidv 
 |-  ( s e. ~P B -> ( A. x ( x e. s -> x e. ( I ` s ) ) <-> A. x ( x e. B -> ( x e. s -> x e. ( I ` s ) ) ) ) )
13 dfss2 
 |-  ( s C_ ( I ` s ) <-> A. x ( x e. s -> x e. ( I ` s ) ) )
14 df-ral 
 |-  ( A. x e. B ( x e. s -> x e. ( I ` s ) ) <-> A. x ( x e. B -> ( x e. s -> x e. ( I ` s ) ) ) )
15 12 13 14 3bitr4g 
 |-  ( s e. ~P B -> ( s C_ ( I ` s ) <-> A. x e. B ( x e. s -> x e. ( I ` s ) ) ) )
16 4 15 syl 
 |-  ( ( ph /\ s e. ~P B ) -> ( s C_ ( I ` s ) <-> A. x e. B ( x e. s -> x e. ( I ` s ) ) ) )
17 3 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> I F N )
18 simpr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> x e. B )
19 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> s e. ~P B )
20 1 2 17 18 19 ntrneiel 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
21 20 imbi2d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( ( x e. s -> x e. ( I ` s ) ) <-> ( x e. s -> s e. ( N ` x ) ) ) )
22 21 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x e. B ( x e. s -> x e. ( I ` s ) ) <-> A. x e. B ( x e. s -> s e. ( N ` x ) ) ) )
23 16 22 bitrd 
 |-  ( ( ph /\ s e. ~P B ) -> ( s C_ ( I ` s ) <-> A. x e. B ( x e. s -> s e. ( N ` x ) ) ) )
24 23 ralbidva 
 |-  ( ph -> ( A. s e. ~P B s C_ ( I ` s ) <-> A. s e. ~P B A. x e. B ( x e. s -> s e. ( N ` x ) ) ) )
25 ralcom 
 |-  ( A. s e. ~P B A. x e. B ( x e. s -> s e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B ( x e. s -> s e. ( N ` x ) ) )
26 24 25 bitrdi 
 |-  ( ph -> ( A. s e. ~P B s C_ ( I ` s ) <-> A. x e. B A. s e. ~P B ( x e. s -> s e. ( N ` x ) ) ) )