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 ( 𝐽 ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) → ( ( 𝐶 ∩ 𝐷 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑠 = 𝐶 )
2 simpr ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → 𝑡 = 𝐷 )
3 2 fveq2d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) )
4 1 3 ineq12d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ( 𝐶 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) ) )
5 4 eqeq1d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ↔ ( 𝐶 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) ) = ∅ ) )
6 1 fveq2d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) )
7 6 2 ineq12d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) ∩ 𝐷 ) )
8 7 eqeq1d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) ∩ 𝐷 ) = ∅ ) )
9 5 8 anbi12d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) ↔ ( ( 𝐶 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) ∩ 𝐷 ) = ∅ ) ) )
10 1 sseq1d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑠 ⊆ 𝑛 ↔ 𝐶 ⊆ 𝑛 ) )
11 2 sseq1d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( 𝑡 ⊆ 𝑚 ↔ 𝐷 ⊆ 𝑚 ) )
12 10 11 3anbi12d ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
13 12 2rexbidv ⊢ ( ( 𝑠 = 𝐶 ∧ 𝑡 = 𝐷 ) → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
14 iscnrm3llem1 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐶 ∈ 𝒫 ∪ 𝐽 ∧ 𝐷 ∈ 𝒫 ∪ 𝐽 ) )
15 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐽 ∈ Top )
16 eqidd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ∪ 𝐽 = ∪ 𝐽 )
17 simp21 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝑍 ∈ 𝒫 ∪ 𝐽 )
18 17 elpwid ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝑍 ⊆ ∪ 𝐽 )
19 eqidd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐽 ↾t 𝑍 ) = ( 𝐽 ↾t 𝑍 ) )
20 simp22 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) )
21 simp3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐶 ∩ 𝐷 ) = ∅ )
22 simp23 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) )
23 15 16 18 19 20 21 22 restclssep ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ( 𝐶 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) ∩ 𝐷 ) = ∅ ) )
24 iscnrm3llem2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
25 23 24 embantd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ( ( ( 𝐶 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐷 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝐶 ) ∩ 𝐷 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
26 9 13 14 25 iscnrm3lem5 ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) → ( ( 𝐶 ∩ 𝐷 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) ) )