Metamath Proof Explorer

Theorem ntrneik13

Description: The interior of the intersection of any pair equals intersection of interiors if and only if the intersection of any pair belonging to the neighborhood of a point is equivalent to both of the pair belonging to the neighborhood of that point. (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 ntrneik13 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ 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 t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. ( I ` ( s i^i t ) ) x e. ( ( I ` s ) i^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 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> I : ~P B --> ~P B )
9 1 2 3 ntrneibex 
 |-  ( ph -> B e. _V )
10 9 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> B e. _V )
11 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> s e. ~P B )
12 elpwi 
 |-  ( s e. ~P B -> s C_ B )
13 ssinss1 
 |-  ( s C_ B -> ( s i^i t ) C_ B )
14 11 12 13 3syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( s i^i t ) C_ B )
15 10 14 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( s i^i t ) e. ~P B )
16 8 15 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` ( s i^i t ) ) e. ~P B )
17 16 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` ( s i^i t ) ) C_ B )
18 ralss 
 |-  ( ( I ` ( s i^i t ) ) C_ B -> ( A. x e. ( I ` ( s i^i t ) ) x e. ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s i^i t ) ) -> x e. ( ( I ` s ) i^i ( I ` t ) ) ) ) )
19 17 18 syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( I ` ( s i^i t ) ) x e. ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s i^i t ) ) -> x e. ( ( I ` s ) i^i ( I ` t ) ) ) ) )
20 4 19 syl5bb 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s i^i t ) ) -> x e. ( ( I ` s ) i^i ( I ` t ) ) ) ) )
21 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 ) ) )
22 7 ffvelrnda 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
23 22 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B )
24 ssinss1 
 |-  ( ( I ` s ) C_ B -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
25 23 24 syl 
 |-  ( ( ph /\ s e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
26 25 adantr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B )
27 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 ) ) ) ) )
28 26 27 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 ) ) ) ) )
29 21 28 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 ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) )
30 20 29 anbi12d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) <-> ( A. x e. B ( x e. ( I ` ( s i^i t ) ) -> x e. ( ( I ` s ) i^i ( I ` t ) ) ) /\ A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) ) )
31 eqss 
 |-  ( ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) )
32 ralbiim 
 |-  ( A. x e. B ( x e. ( I ` ( s i^i t ) ) <-> x e. ( ( I ` s ) i^i ( I ` t ) ) ) <-> ( A. x e. B ( x e. ( I ` ( s i^i t ) ) -> x e. ( ( I ` s ) i^i ( I ` t ) ) ) /\ A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) )
33 30 31 32 3bitr4g 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s i^i t ) ) <-> x e. ( ( I ` s ) i^i ( I ` t ) ) ) ) )
34 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
35 simpr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
36 9 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> B e. _V )
37 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
38 37 elpwid 
 |-  ( ( ph /\ s e. ~P B ) -> s C_ B )
39 38 13 syl 
 |-  ( ( ph /\ s e. ~P B ) -> ( s i^i t ) C_ B )
40 36 39 sselpwd 
 |-  ( ( ph /\ s e. ~P B ) -> ( s i^i t ) e. ~P B )
41 40 ad2antrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s i^i t ) e. ~P B )
42 1 2 34 35 41 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 ) ) )
43 elin 
 |-  ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( x e. ( I ` s ) /\ x e. ( I ` t ) ) )
44 simpllr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
45 1 2 34 35 44 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
46 simplr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
47 1 2 34 35 46 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
48 45 47 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 ) ) ) )
49 43 48 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 ) ) ) )
50 42 49 bibi12d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` ( s i^i t ) ) <-> x e. ( ( I ` s ) i^i ( I ` t ) ) ) <-> ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
51 50 ralbidva 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( x e. ( I ` ( s i^i t ) ) <-> x e. ( ( I ` s ) i^i ( I ` t ) ) ) <-> A. x e. B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
52 33 51 bitrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
53 52 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. t e. ~P B A. x e. B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
54 ralcom 
 |-  ( A. t e. ~P B A. x e. B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) <-> A. x e. B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) )
55 53 54 bitrdi 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
56 55 ralbidva 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )
57 ralcom 
 |-  ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) )
58 56 57 bitrdi 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s i^i t ) e. ( N ` x ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) )