Metamath Proof Explorer


Theorem ntrclsk13

Description: The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (Contributed by RP, 19-Jun-2021)

Ref Expression
Hypotheses ntrcls.o O = i V k 𝒫 i 𝒫 i j 𝒫 i i k i j
ntrcls.d D = O B
ntrcls.r φ I D K
Assertion ntrclsk13 φ s 𝒫 B t 𝒫 B I s t = I s I t s 𝒫 B t 𝒫 B K s t = K s K t

Proof

Step Hyp Ref Expression
1 ntrcls.o O = i V k 𝒫 i 𝒫 i j 𝒫 i i k i j
2 ntrcls.d D = O B
3 ntrcls.r φ I D K
4 ineq1 s = a s t = a t
5 4 fveq2d s = a I s t = I a t
6 fveq2 s = a I s = I a
7 6 ineq1d s = a I s I t = I a I t
8 5 7 eqeq12d s = a I s t = I s I t I a t = I a I t
9 ineq2 t = b a t = a b
10 9 fveq2d t = b I a t = I a b
11 fveq2 t = b I t = I b
12 11 ineq2d t = b I a I t = I a I b
13 10 12 eqeq12d t = b I a t = I a I t I a b = I a I b
14 8 13 cbvral2vw s 𝒫 B t 𝒫 B I s t = I s I t a 𝒫 B b 𝒫 B I a b = I a I b
15 2 3 ntrclsbex φ B V
16 difssd φ B s B
17 15 16 sselpwd φ B s 𝒫 B
18 17 adantr φ s 𝒫 B B s 𝒫 B
19 elpwi a 𝒫 B a B
20 15 adantr φ a B B V
21 difssd φ a B B a B
22 20 21 sselpwd φ a B B a 𝒫 B
23 difeq2 s = B a B s = B B a
24 23 eqeq2d s = B a a = B s a = B B a
25 eqcom a = B B a B B a = a
26 24 25 bitrdi s = B a a = B s B B a = a
27 26 adantl φ a B s = B a a = B s B B a = a
28 dfss4 a B B B a = a
29 28 biimpi a B B B a = a
30 29 adantl φ a B B B a = a
31 22 27 30 rspcedvd φ a B s 𝒫 B a = B s
32 19 31 sylan2 φ a 𝒫 B s 𝒫 B a = B s
33 ineq1 a = B s a b = B s b
34 33 fveq2d a = B s I a b = I B s b
35 fveq2 a = B s I a = I B s
36 35 ineq1d a = B s I a I b = I B s I b
37 34 36 eqeq12d a = B s I a b = I a I b I B s b = I B s I b
38 37 ralbidv a = B s b 𝒫 B I a b = I a I b b 𝒫 B I B s b = I B s I b
39 38 3ad2ant3 φ s 𝒫 B a = B s b 𝒫 B I a b = I a I b b 𝒫 B I B s b = I B s I b
40 difssd φ B t B
41 15 40 sselpwd φ B t 𝒫 B
42 41 ad2antrr φ s 𝒫 B t 𝒫 B B t 𝒫 B
43 simpll φ s 𝒫 B b 𝒫 B φ
44 elpwi b 𝒫 B b B
45 44 adantl φ s 𝒫 B b 𝒫 B b B
46 difssd φ B b B
47 15 46 sselpwd φ B b 𝒫 B
48 47 adantr φ b B B b 𝒫 B
49 difeq2 t = B b B t = B B b
50 49 eqeq2d t = B b b = B t b = B B b
51 eqcom b = B B b B B b = b
52 50 51 bitrdi t = B b b = B t B B b = b
53 52 adantl φ b B t = B b b = B t B B b = b
54 dfss4 b B B B b = b
55 54 biimpi b B B B b = b
56 55 adantl φ b B B B b = b
57 48 53 56 rspcedvd φ b B t 𝒫 B b = B t
58 43 45 57 syl2anc φ s 𝒫 B b 𝒫 B t 𝒫 B b = B t
59 ineq2 b = B t B s b = B s B t
60 difundi B s t = B s B t
61 59 60 eqtr4di b = B t B s b = B s t
62 61 fveq2d b = B t I B s b = I B s t
63 fveq2 b = B t I b = I B t
64 63 ineq2d b = B t I B s I b = I B s I B t
65 62 64 eqeq12d b = B t I B s b = I B s I b I B s t = I B s I B t
66 65 3ad2ant3 φ s 𝒫 B t 𝒫 B b = B t I B s b = I B s I b I B s t = I B s I B t
67 simp1l φ s 𝒫 B t 𝒫 B b = B t φ
68 67 15 jccir φ s 𝒫 B t 𝒫 B b = B t φ B V
69 simp1r φ s 𝒫 B t 𝒫 B b = B t s 𝒫 B
70 simp2 φ s 𝒫 B t 𝒫 B b = B t t 𝒫 B
71 1 2 3 ntrclsiex φ I 𝒫 B 𝒫 B
72 elmapi I 𝒫 B 𝒫 B I : 𝒫 B 𝒫 B
73 71 72 syl φ I : 𝒫 B 𝒫 B
74 73 anim1i φ B V I : 𝒫 B 𝒫 B B V
75 74 adantr φ B V s 𝒫 B t 𝒫 B I : 𝒫 B 𝒫 B B V
76 simpl I : 𝒫 B 𝒫 B B V I : 𝒫 B 𝒫 B
77 simpr I : 𝒫 B 𝒫 B B V B V
78 difssd I : 𝒫 B 𝒫 B B V B s t B
79 77 78 sselpwd I : 𝒫 B 𝒫 B B V B s t 𝒫 B
80 76 79 ffvelrnd I : 𝒫 B 𝒫 B B V I B s t 𝒫 B
81 80 elpwid I : 𝒫 B 𝒫 B B V I B s t B
82 difssd I : 𝒫 B 𝒫 B B V B s B
83 77 82 sselpwd I : 𝒫 B 𝒫 B B V B s 𝒫 B
84 76 83 ffvelrnd I : 𝒫 B 𝒫 B B V I B s 𝒫 B
85 84 elpwid I : 𝒫 B 𝒫 B B V I B s B
86 ssinss1 I B s B I B s I B t B
87 85 86 syl I : 𝒫 B 𝒫 B B V I B s I B t B
88 81 87 jca I : 𝒫 B 𝒫 B B V I B s t B I B s I B t B
89 rcompleq I B s t B I B s I B t B I B s t = I B s I B t B I B s t = B I B s I B t
90 75 88 89 3syl φ B V s 𝒫 B t 𝒫 B I B s t = I B s I B t B I B s t = B I B s I B t
91 simplr φ B V s 𝒫 B t 𝒫 B B V
92 71 ad2antrr φ B V s 𝒫 B t 𝒫 B I 𝒫 B 𝒫 B
93 eqid D I = D I
94 simprl φ B V s 𝒫 B t 𝒫 B s 𝒫 B
95 94 elpwid φ B V s 𝒫 B t 𝒫 B s B
96 simprr φ B V s 𝒫 B t 𝒫 B t 𝒫 B
97 96 elpwid φ B V s 𝒫 B t 𝒫 B t B
98 95 97 unssd φ B V s 𝒫 B t 𝒫 B s t B
99 91 98 sselpwd φ B V s 𝒫 B t 𝒫 B s t 𝒫 B
100 eqid D I s t = D I s t
101 1 2 91 92 93 99 100 dssmapfv3d φ B V s 𝒫 B t 𝒫 B D I s t = B I B s t
102 simpl s 𝒫 B t 𝒫 B s 𝒫 B
103 simplr φ B V s 𝒫 B B V
104 71 ad2antrr φ B V s 𝒫 B I 𝒫 B 𝒫 B
105 simpr φ B V s 𝒫 B s 𝒫 B
106 eqid D I s = D I s
107 1 2 103 104 93 105 106 dssmapfv3d φ B V s 𝒫 B D I s = B I B s
108 102 107 sylan2 φ B V s 𝒫 B t 𝒫 B D I s = B I B s
109 simpr s 𝒫 B t 𝒫 B t 𝒫 B
110 simplr φ B V t 𝒫 B B V
111 71 ad2antrr φ B V t 𝒫 B I 𝒫 B 𝒫 B
112 simpr φ B V t 𝒫 B t 𝒫 B
113 eqid D I t = D I t
114 1 2 110 111 93 112 113 dssmapfv3d φ B V t 𝒫 B D I t = B I B t
115 109 114 sylan2 φ B V s 𝒫 B t 𝒫 B D I t = B I B t
116 108 115 uneq12d φ B V s 𝒫 B t 𝒫 B D I s D I t = B I B s B I B t
117 difindi B I B s I B t = B I B s B I B t
118 116 117 eqtr4di φ B V s 𝒫 B t 𝒫 B D I s D I t = B I B s I B t
119 101 118 eqeq12d φ B V s 𝒫 B t 𝒫 B D I s t = D I s D I t B I B s t = B I B s I B t
120 simpll φ B V s 𝒫 B t 𝒫 B φ
121 1 2 3 ntrclsfv1 φ D I = K
122 fveq1 D I = K D I s t = K s t
123 fveq1 D I = K D I s = K s
124 fveq1 D I = K D I t = K t
125 123 124 uneq12d D I = K D I s D I t = K s K t
126 122 125 eqeq12d D I = K D I s t = D I s D I t K s t = K s K t
127 120 121 126 3syl φ B V s 𝒫 B t 𝒫 B D I s t = D I s D I t K s t = K s K t
128 90 119 127 3bitr2d φ B V s 𝒫 B t 𝒫 B I B s t = I B s I B t K s t = K s K t
129 68 69 70 128 syl12anc φ s 𝒫 B t 𝒫 B b = B t I B s t = I B s I B t K s t = K s K t
130 66 129 bitrd φ s 𝒫 B t 𝒫 B b = B t I B s b = I B s I b K s t = K s K t
131 42 58 130 ralxfrd2 φ s 𝒫 B b 𝒫 B I B s b = I B s I b t 𝒫 B K s t = K s K t
132 131 3adant3 φ s 𝒫 B a = B s b 𝒫 B I B s b = I B s I b t 𝒫 B K s t = K s K t
133 39 132 bitrd φ s 𝒫 B a = B s b 𝒫 B I a b = I a I b t 𝒫 B K s t = K s K t
134 18 32 133 ralxfrd2 φ a 𝒫 B b 𝒫 B I a b = I a I b s 𝒫 B t 𝒫 B K s t = K s K t
135 14 134 syl5bb φ s 𝒫 B t 𝒫 B I s t = I s I t s 𝒫 B t 𝒫 B K s t = K s K t