Theorem iscnrm4

Description: A completely normal topology is a topology in which two separated sets can be separated by neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		iscnrm3	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
2		id	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ Top )
3	2	sepnsepo	⊢ ( 𝐽 ∈ Top → ( ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑠 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑡 ) ( 𝑛 ∩ 𝑚 ) = ∅ ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
4	3	imbi2d	⊢ ( 𝐽 ∈ Top → ( ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑠 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑡 ) ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
5	4	2ralbidv	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑠 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑡 ) ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
6	5	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑠 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑡 ) ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
7	1 6	bitr4i	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑠 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑡 ) ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )