Metamath Proof Explorer

Theorem iscnrm3r

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

Ref Expression
Assertion iscnrm3r ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) → ( ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( 𝐽 ↾t 𝑧 ) = ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
2 1 fveq2d ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) = ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) )
3 1 rexeqdv ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ↔ ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
4 1 3 rexeqbidv ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ↔ ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
5 4 imbi2d ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
6 2 5 raleqbidv ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
7 2 6 raleqbidv ⊢ ( 𝑧 = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) → ( ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
8 7 rspcv ⊢ ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
9 8 3ad2ant1 ⊢ ( ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
10 ineq12 ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑐 ∩ 𝑑 ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
11 10 eqeq1d ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ ↔ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ ) )
12 simpl ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) )
13 12 sseq1d ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑐 ⊆ 𝑙 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ) )
14 simpr ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
15 14 sseq1d ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑑 ⊆ 𝑘 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ) )
16 13 15 3anbi12d ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ↔ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
17 16 2rexbidv ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ↔ ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
18 11 17 imbi12d ⊢ ( ( 𝑐 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∧ 𝑑 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
19 18 rspc2gv ⊢ ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) → ( ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
20 19 3adant1 ⊢ ( ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) → ( ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
21 9 20 syld ⊢ ( ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
22 iscnrm3rlem3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) )
23 22 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) )
24 disjdifb ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅
25 24 a1i ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ )
26 iscnrm3rlem8 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
27 25 26 embantd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∩ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
28 21 23 27 iscnrm3lem4 ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) → ( ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) ) )