Metamath Proof Explorer


Theorem iscnrm3llem2

Description: Lemma for iscnrm3l . If there exist disjoint open neighborhoods in the orignal topology for two disjoint closed sets in a subspace, then they can be separated by open neighborhoods in the subspace topology. (Could shorten proof with ssin0 .) (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3llem2 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = l J 𝑡 Z k J 𝑡 Z C l D k l k =

Proof

Step Hyp Ref Expression
1 sseq2 l = n Z C l C n Z
2 ineq1 l = n Z l k = n Z k
3 2 eqeq1d l = n Z l k = n Z k =
4 1 3 3anbi13d l = n Z C l D k l k = C n Z D k n Z k =
5 sseq2 k = m Z D k D m Z
6 ineq2 k = m Z n Z k = n Z m Z
7 6 eqeq1d k = m Z n Z k = n Z m Z =
8 5 7 3anbi23d k = m Z C n Z D k n Z k = C n Z D m Z n Z m Z =
9 simp11 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = J Top
10 simp121 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = Z 𝒫 J
11 simp2l J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n J
12 elrestr J Top Z 𝒫 J n J n Z J 𝑡 Z
13 9 10 11 12 syl3anc J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n Z J 𝑡 Z
14 simp2r J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = m J
15 elrestr J Top Z 𝒫 J m J m Z J 𝑡 Z
16 9 10 14 15 syl3anc J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = m Z J 𝑡 Z
17 simp31 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = C n
18 eqidd J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = J = J
19 10 elpwid J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = Z J
20 eqidd J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = J 𝑡 Z = J 𝑡 Z
21 simp122 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = C Clsd J 𝑡 Z
22 9 18 19 20 21 restcls2lem J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = C Z
23 17 22 ssind J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = C n Z
24 simp32 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = D m
25 simp123 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = D Clsd J 𝑡 Z
26 9 18 19 20 25 restcls2lem J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = D Z
27 24 26 ssind J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = D m Z
28 inss1 n Z n
29 inss1 m Z m
30 ss2in n Z n m Z m n Z m Z n m
31 28 29 30 mp2an n Z m Z n m
32 simp33 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n m =
33 31 32 sseqtrid J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n Z m Z
34 ss0 n Z m Z n Z m Z =
35 33 34 syl J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n Z m Z =
36 23 27 35 3jca J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = C n Z D m Z n Z m Z =
37 13 16 36 3jca J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = n Z J 𝑡 Z m Z J 𝑡 Z C n Z D m Z n Z m Z =
38 4 8 37 iscnrm3lem7 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = n J m J C n D m n m = l J 𝑡 Z k J 𝑡 Z C l D k l k =