Metamath Proof Explorer

Theorem ntrneikb

Description: The interiors of disjoint sets are disjoint if and only if the neighborhoods of every point contain no disjoint sets. (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 ntrneikb 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( 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 e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )

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 con34b 
 |-  ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> ( -. ( s i^i t ) =/= (/) -> -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) )
5 4 albii 
 |-  ( A. x ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x ( -. ( s i^i t ) =/= (/) -> -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) )
6 19.21v 
 |-  ( A. x ( -. ( s i^i t ) =/= (/) -> -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) <-> ( -. ( s i^i t ) =/= (/) -> A. x -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) )
7 nne 
 |-  ( -. ( s i^i t ) =/= (/) <-> ( s i^i t ) = (/) )
8 elin 
 |-  ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( x e. ( I ` s ) /\ x e. ( I ` t ) ) )
9 8 imbi1i 
 |-  ( ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. (/) ) <-> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> x e. (/) ) )
10 noel 
 |-  -. x e. (/)
11 imnot 
 |-  ( -. x e. (/) -> ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> x e. (/) ) <-> -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) )
12 10 11 ax-mp 
 |-  ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> x e. (/) ) <-> -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) )
13 9 12 bitr2i 
 |-  ( -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) <-> ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. (/) ) )
14 13 albii 
 |-  ( A. x -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) <-> A. x ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. (/) ) )
15 df-ss 
 |-  ( ( ( I ` s ) i^i ( I ` t ) ) C_ (/) <-> A. x ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. (/) ) )
16 ss0b 
 |-  ( ( ( I ` s ) i^i ( I ` t ) ) C_ (/) <-> ( ( I ` s ) i^i ( I ` t ) ) = (/) )
17 14 15 16 3bitr2i 
 |-  ( A. x -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) <-> ( ( I ` s ) i^i ( I ` t ) ) = (/) )
18 7 17 imbi12i 
 |-  ( ( -. ( s i^i t ) =/= (/) -> A. x -. ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) <-> ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )
19 5 6 18 3bitrri 
 |-  ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> A. x ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) )
20 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
21 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
22 20 21 syl 
 |-  ( ph -> I : ~P B --> ~P B )
23 22 ffvelcdmda 
 |-  ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B )
24 23 adantr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) e. ~P B )
25 24 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) C_ B )
26 25 sseld 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( x e. ( I ` s ) -> x e. B ) )
27 26 adantrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> x e. B ) )
28 27 imp 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) -> x e. B )
29 biimt 
 |-  ( x e. B -> ( ( s i^i t ) =/= (/) <-> ( x e. B -> ( s i^i t ) =/= (/) ) ) )
30 28 29 syl 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) -> ( ( s i^i t ) =/= (/) <-> ( x e. B -> ( s i^i t ) =/= (/) ) ) )
31 30 pm5.74da 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( x e. B -> ( s i^i t ) =/= (/) ) ) ) )
32 bi2.04 
 |-  ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( x e. B -> ( s i^i t ) =/= (/) ) ) <-> ( x e. B -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) ) )
33 31 32 bitrdi 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> ( x e. B -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) ) ) )
34 33 albidv 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x ( x e. B -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) ) ) )
35 df-ral 
 |-  ( A. x e. B ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x ( x e. B -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) ) )
36 34 35 bitr4di 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x e. B ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) ) )
37 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
38 simpr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
39 simpllr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
40 1 2 37 38 39 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
41 simplr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
42 1 2 37 38 41 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
43 40 42 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 ) ) ) )
44 43 imbi1d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
45 44 ralbidva 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
46 36 45 bitrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) -> ( s i^i t ) =/= (/) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
47 19 46 bitrid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
48 47 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
49 48 ralbidva 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> A. s e. ~P B A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )
50 ralrot3 
 |-  ( A. s e. ~P B A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( 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 ) =/= (/) ) )
51 49 50 bitrdi 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( 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 e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) =/= (/) ) ) )