Metamath Proof Explorer


Theorem iscnrm3l

Description: Lemma for iscnrm3 . Given a topology J , if two separated sets can be separated by open neighborhoods, then all subspaces of the topology J are normal, i.e., two disjoint closed sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3l J Top s 𝒫 J t 𝒫 J s cls J t = cls J s t = n J m J s n t m n m = Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = l J 𝑡 Z k J 𝑡 Z C l D k l k =

Proof

Step Hyp Ref Expression
1 simpl s = C t = D s = C
2 simpr s = C t = D t = D
3 2 fveq2d s = C t = D cls J t = cls J D
4 1 3 ineq12d s = C t = D s cls J t = C cls J D
5 4 eqeq1d s = C t = D s cls J t = C cls J D =
6 1 fveq2d s = C t = D cls J s = cls J C
7 6 2 ineq12d s = C t = D cls J s t = cls J C D
8 7 eqeq1d s = C t = D cls J s t = cls J C D =
9 5 8 anbi12d s = C t = D s cls J t = cls J s t = C cls J D = cls J C D =
10 1 sseq1d s = C t = D s n C n
11 2 sseq1d s = C t = D t m D m
12 10 11 3anbi12d s = C t = D s n t m n m = C n D m n m =
13 12 2rexbidv s = C t = D n J m J s n t m n m = n J m J C n D m n m =
14 iscnrm3llem1 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = C 𝒫 J D 𝒫 J
15 simp1 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = J Top
16 eqidd J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = J = J
17 simp21 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = Z 𝒫 J
18 17 elpwid J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = Z J
19 eqidd J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = J 𝑡 Z = J 𝑡 Z
20 simp22 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = C Clsd J 𝑡 Z
21 simp3 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = C D =
22 simp23 J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = D Clsd J 𝑡 Z
23 15 16 18 19 20 21 22 restclssep J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = C cls J D = cls J C D =
24 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 =
25 23 24 embantd J Top Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = C cls J D = cls J C D = n J m J C n D m n m = l J 𝑡 Z k J 𝑡 Z C l D k l k =
26 9 13 14 25 iscnrm3lem5 J Top s 𝒫 J t 𝒫 J s cls J t = cls J s t = n J m J s n t m n m = Z 𝒫 J C Clsd J 𝑡 Z D Clsd J 𝑡 Z C D = l J 𝑡 Z k J 𝑡 Z C l D k l k =