Theorem iscnrm3v

Description: A topology is completely normal iff two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 10-Sep-2024)

	Ref	Expression
Assertion	iscnrm3v	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ CNrm ↔ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
2	1	baib	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ CNrm ↔ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )