Metamath Proof Explorer

Theorem ntrclskb

Description: The interiors of disjoint sets are disjoint if and only if the closures of sets that span the base set also span the base set. (Contributed by RP, 10-Jun-2021)

Ref Expression
Hypotheses ntrcls.o 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
Assertion ntrclskb 
|- ( 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 ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 ineq1 
 |-  ( s = a -> ( s i^i t ) = ( a i^i t ) )
5 4 eqeq1d 
 |-  ( s = a -> ( ( s i^i t ) = (/) <-> ( a i^i t ) = (/) ) )
6 fveq2 
 |-  ( s = a -> ( I ` s ) = ( I ` a ) )
7 6 ineq1d 
 |-  ( s = a -> ( ( I ` s ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` t ) ) )
8 7 eqeq1d 
 |-  ( s = a -> ( ( ( I ` s ) i^i ( I ` t ) ) = (/) <-> ( ( I ` a ) i^i ( I ` t ) ) = (/) ) )
9 5 8 imbi12d 
 |-  ( s = a -> ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> ( ( a i^i t ) = (/) -> ( ( I ` a ) i^i ( I ` t ) ) = (/) ) ) )
10 ineq2 
 |-  ( t = b -> ( a i^i t ) = ( a i^i b ) )
11 10 eqeq1d 
 |-  ( t = b -> ( ( a i^i t ) = (/) <-> ( a i^i b ) = (/) ) )
12 fveq2 
 |-  ( t = b -> ( I ` t ) = ( I ` b ) )
13 12 ineq2d 
 |-  ( t = b -> ( ( I ` a ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` b ) ) )
14 13 eqeq1d 
 |-  ( t = b -> ( ( ( I ` a ) i^i ( I ` t ) ) = (/) <-> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) )
15 11 14 imbi12d 
 |-  ( t = b -> ( ( ( a i^i t ) = (/) -> ( ( I ` a ) i^i ( I ` t ) ) = (/) ) <-> ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) ) )
16 9 15 cbvral2vw 
 |-  ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> A. a e. ~P B A. b e. ~P B ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) )
17 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ s ) e. ~P B )
18 17 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) e. ~P B )
19 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ a ) e. ~P B )
20 19 adantr 
 |-  ( ( ph /\ a e. ~P B ) -> ( B \ a ) e. ~P B )
21 difeq2 
 |-  ( s = ( B \ a ) -> ( B \ s ) = ( B \ ( B \ a ) ) )
22 21 eqeq2d 
 |-  ( s = ( B \ a ) -> ( a = ( B \ s ) <-> a = ( B \ ( B \ a ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ a e. ~P B ) /\ s = ( B \ a ) ) -> ( a = ( B \ s ) <-> a = ( B \ ( B \ a ) ) ) )
24 elpwi 
 |-  ( a e. ~P B -> a C_ B )
25 dfss4 
 |-  ( a C_ B <-> ( B \ ( B \ a ) ) = a )
26 24 25 sylib 
 |-  ( a e. ~P B -> ( B \ ( B \ a ) ) = a )
27 26 eqcomd 
 |-  ( a e. ~P B -> a = ( B \ ( B \ a ) ) )
28 27 adantl 
 |-  ( ( ph /\ a e. ~P B ) -> a = ( B \ ( B \ a ) ) )
29 20 23 28 rspcedvd 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
30 simpl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ph )
31 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ t ) e. ~P B )
32 30 31 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
33 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ b ) e. ~P B )
34 33 adantr 
 |-  ( ( ph /\ b e. ~P B ) -> ( B \ b ) e. ~P B )
35 difeq2 
 |-  ( t = ( B \ b ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
36 35 eqeq2d 
 |-  ( t = ( B \ b ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
37 36 adantl 
 |-  ( ( ( ph /\ b e. ~P B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
38 elpwi 
 |-  ( b e. ~P B -> b C_ B )
39 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
40 38 39 sylib 
 |-  ( b e. ~P B -> ( B \ ( B \ b ) ) = b )
41 40 eqcomd 
 |-  ( b e. ~P B -> b = ( B \ ( B \ b ) ) )
42 41 adantl 
 |-  ( ( ph /\ b e. ~P B ) -> b = ( B \ ( B \ b ) ) )
43 34 37 42 rspcedvd 
 |-  ( ( ph /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
44 43 3ad2antl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
45 simp13 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> a = ( B \ s ) )
46 ineq1 
 |-  ( a = ( B \ s ) -> ( a i^i b ) = ( ( B \ s ) i^i b ) )
47 46 eqeq1d 
 |-  ( a = ( B \ s ) -> ( ( a i^i b ) = (/) <-> ( ( B \ s ) i^i b ) = (/) ) )
48 fveq2 
 |-  ( a = ( B \ s ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
49 48 ineq1d 
 |-  ( a = ( B \ s ) -> ( ( I ` a ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) )
50 49 eqeq1d 
 |-  ( a = ( B \ s ) -> ( ( ( I ` a ) i^i ( I ` b ) ) = (/) <-> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) ) )
51 47 50 imbi12d 
 |-  ( a = ( B \ s ) -> ( ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) <-> ( ( ( B \ s ) i^i b ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) ) ) )
52 45 51 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) <-> ( ( ( B \ s ) i^i b ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) ) ) )
53 simp3 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> b = ( B \ t ) )
54 ineq2 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( ( B \ s ) i^i ( B \ t ) ) )
55 54 eqeq1d 
 |-  ( b = ( B \ t ) -> ( ( ( B \ s ) i^i b ) = (/) <-> ( ( B \ s ) i^i ( B \ t ) ) = (/) ) )
56 fveq2 
 |-  ( b = ( B \ t ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
57 56 ineq2d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) )
58 57 eqeq1d 
 |-  ( b = ( B \ t ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) <-> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) )
59 55 58 imbi12d 
 |-  ( b = ( B \ t ) -> ( ( ( ( B \ s ) i^i b ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) ) <-> ( ( ( B \ s ) i^i ( B \ t ) ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) ) )
60 53 59 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( ( B \ s ) i^i b ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = (/) ) <-> ( ( ( B \ s ) i^i ( B \ t ) ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) ) )
61 simp11 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
62 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
63 simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
64 simp2 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> s e. ~P B )
65 64 elpwid 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> s C_ B )
66 simp3 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> t e. ~P B )
67 66 elpwid 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> t C_ B )
68 65 67 unssd 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( s u. t ) C_ B )
69 ssid 
 |-  B C_ B
70 rcompleq 
 |-  ( ( ( s u. t ) C_ B /\ B C_ B ) -> ( ( s u. t ) = B <-> ( B \ ( s u. t ) ) = ( B \ B ) ) )
71 68 69 70 sylancl 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( s u. t ) = B <-> ( B \ ( s u. t ) ) = ( B \ B ) ) )
72 difundi 
 |-  ( B \ ( s u. t ) ) = ( ( B \ s ) i^i ( B \ t ) )
73 difid 
 |-  ( B \ B ) = (/)
74 72 73 eqeq12i 
 |-  ( ( B \ ( s u. t ) ) = ( B \ B ) <-> ( ( B \ s ) i^i ( B \ t ) ) = (/) )
75 71 74 bitr2di 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( B \ s ) i^i ( B \ t ) ) = (/) <-> ( s u. t ) = B ) )
76 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
77 76 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
78 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
79 77 78 syl 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> I : ~P B --> ~P B )
80 2 3 ntrclsbex 
 |-  ( ph -> B e. _V )
81 80 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> B e. _V )
82 difssd 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( B \ s ) C_ B )
83 81 82 sselpwd 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( B \ s ) e. ~P B )
84 79 83 ffvelcdmd 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( I ` ( B \ s ) ) e. ~P B )
85 84 elpwid 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( I ` ( B \ s ) ) C_ B )
86 ssinss1 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
87 85 86 syl 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
88 0ss 
 |-  (/) C_ B
89 rcompleq 
 |-  ( ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B /\ (/) C_ B ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) <-> ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( B \ (/) ) ) )
90 87 88 89 sylancl 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) <-> ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( B \ (/) ) ) )
91 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
92 dif0 
 |-  ( B \ (/) ) = B
93 91 92 eqeq12i 
 |-  ( ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( B \ (/) ) <-> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = B )
94 90 93 bitrdi 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) <-> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = B ) )
95 75 94 imbi12d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( ( B \ s ) i^i ( B \ t ) ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) <-> ( ( s u. t ) = B -> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = B ) ) )
96 eqid 
 |-  ( D ` I ) = ( D ` I )
97 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
98 1 2 81 77 96 64 97 dssmapfv3d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
99 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
100 1 2 81 77 96 66 99 dssmapfv3d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
101 98 100 uneq12d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) )
102 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
103 102 3ad2ant1 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( D ` I ) = K )
104 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` s ) = ( K ` s ) )
105 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` t ) = ( K ` t ) )
106 104 105 uneq12d 
 |-  ( ( D ` I ) = K -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( K ` s ) u. ( K ` t ) ) )
107 103 106 syl 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( K ` s ) u. ( K ` t ) ) )
108 101 107 eqtr3d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = ( ( K ` s ) u. ( K ` t ) ) )
109 108 eqeq1d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = B <-> ( ( K ` s ) u. ( K ` t ) ) = B ) )
110 109 imbi2d 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( s u. t ) = B -> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = B ) <-> ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
111 95 110 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ t e. ~P B ) -> ( ( ( ( B \ s ) i^i ( B \ t ) ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) <-> ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
112 61 62 63 111 syl3anc 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( ( B \ s ) i^i ( B \ t ) ) = (/) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) = (/) ) <-> ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
113 52 60 112 3bitrd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) <-> ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
114 32 44 113 ralxfrd2 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) <-> A. t e. ~P B ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
115 18 29 114 ralxfrd2 
 |-  ( ph -> ( A. a e. ~P B A. b e. ~P B ( ( a i^i b ) = (/) -> ( ( I ` a ) i^i ( I ` b ) ) = (/) ) <-> A. s e. ~P B A. t e. ~P B ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )
116 16 115 bitrid 
 |-  ( 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 ( ( s u. t ) = B -> ( ( K ` s ) u. ( K ` t ) ) = B ) ) )