Metamath Proof Explorer

Theorem ntrneik2

Description: An interior function is contracting if and only if all the neighborhoods of a point contain 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 ntrneik2 
|- ( ph -> ( A. s e. ~P B ( I ` s ) C_ s <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) -> x e. 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 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
5 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
6 4 5 syl 
 |-  ( ph -> I : ~P B --> ~P B )
7 6 ffvelrnda 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
8 7 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B )
9 8 sselda 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. ( I ` s ) ) -> x e. B )
10 biimt 
 |-  ( x e. B -> ( x e. s <-> ( x e. B -> x e. s ) ) )
11 9 10 syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. ( I ` s ) ) -> ( x e. s <-> ( x e. B -> x e. s ) ) )
12 11 pm5.74da 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( x e. ( I ` s ) -> x e. s ) <-> ( x e. ( I ` s ) -> ( x e. B -> x e. s ) ) ) )
13 bi2.04 
 |-  ( ( x e. ( I ` s ) -> ( x e. B -> x e. s ) ) <-> ( x e. B -> ( x e. ( I ` s ) -> x e. s ) ) )
14 12 13 bitrdi 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( x e. ( I ` s ) -> x e. s ) <-> ( x e. B -> ( x e. ( I ` s ) -> x e. s ) ) ) )
15 14 albidv 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x ( x e. ( I ` s ) -> x e. s ) <-> A. x ( x e. B -> ( x e. ( I ` s ) -> x e. s ) ) ) )
16 dfss2 
 |-  ( ( I ` s ) C_ s <-> A. x ( x e. ( I ` s ) -> x e. s ) )
17 df-ral 
 |-  ( A. x e. B ( x e. ( I ` s ) -> x e. s ) <-> A. x ( x e. B -> ( x e. ( I ` s ) -> x e. s ) ) )
18 15 16 17 3bitr4g 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` s ) C_ s <-> A. x e. B ( x e. ( I ` s ) -> x e. s ) ) )
19 3 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> I F N )
20 simpr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> x e. B )
21 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> s e. ~P B )
22 1 2 19 20 21 ntrneiel 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
23 22 imbi1d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) -> x e. s ) <-> ( s e. ( N ` x ) -> x e. s ) ) )
24 23 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. x e. B ( x e. ( I ` s ) -> x e. s ) <-> A. x e. B ( s e. ( N ` x ) -> x e. s ) ) )
25 18 24 bitrd 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` s ) C_ s <-> A. x e. B ( s e. ( N ` x ) -> x e. s ) ) )
26 25 ralbidva 
 |-  ( ph -> ( A. s e. ~P B ( I ` s ) C_ s <-> A. s e. ~P B A. x e. B ( s e. ( N ` x ) -> x e. s ) ) )
27 ralcom 
 |-  ( A. s e. ~P B A. x e. B ( s e. ( N ` x ) -> x e. s ) <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) -> x e. s ) )
28 26 27 bitrdi 
 |-  ( ph -> ( A. s e. ~P B ( I ` s ) C_ s <-> A. x e. B A. s e. ~P B ( s e. ( N ` x ) -> x e. s ) ) )