Metamath Proof Explorer


Theorem ntrneik3

Description: The intersection of interiors of any pair is a subset of the interior of the intersection if and only if the intersection of any two neighborhoods of a point is also a neighborhood. (Contributed by RP, 19-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 ntrneik3
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) 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 dfss3
 |-  ( ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) )
5 1 2 3 ntrneiiex
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
6 elmapi
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
7 5 6 syl
 |-  ( ph -> I : ~P B --> ~P B )
8 7 ffvelrnda
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
9 8 elpwid
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B )
10 ssinss1
 |-  ( ( I ` s ) C_ B -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
11 9 10 syl
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
12 11 adantr
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
13 ralss
 |-  ( ( ( I ` s ) i^i ( I ` t ) ) C_ B -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) )
14 12 13 syl
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) )
15 elin
 |-  ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( x e. ( I ` s ) /\ x e. ( I ` t ) ) )
16 3 ad3antrrr
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
17 simpr
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
18 simpllr
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
19 1 2 16 17 18 ntrneiel
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
20 simplr
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
21 1 2 16 17 20 ntrneiel
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
22 19 21 anbi12d
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) )
23 15 22 syl5bb
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) )
24 1 2 3 ntrneibex
 |-  ( ph -> B e. _V )
25 24 ad3antrrr
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> B e. _V )
26 18 elpwid
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s C_ B )
27 ssinss1
 |-  ( s C_ B -> ( s i^i t ) C_ B )
28 26 27 syl
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s i^i t ) C_ B )
29 25 28 sselpwd
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s i^i t ) e. ~P B )
30 1 2 16 17 29 ntrneiel
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` ( s i^i t ) ) <-> ( s i^i t ) e. ( N ` x ) ) )
31 23 30 imbi12d
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) <-> ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
32 31 ralbidva
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
33 14 32 bitrd
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
34 4 33 syl5bb
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
35 34 ralbidva
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
36 ralcom
 |-  ( A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) )
37 35 36 bitrdi
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
38 37 ralbidva
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )
39 ralcom
 |-  ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) )
40 38 39 bitrdi
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) )