Theorem isnrm4

Description: A topological space is normal iff any two disjoint closed sets are separated by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024)

	Ref	Expression
Assertion	isnrm4	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnrm3	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
2		id	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ Top )
3	2	sepnsepo	⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
4	3	imbi2d	⊢ ( 𝐽 ∈ Top → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
5	4	2ralbidv	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
6	5	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
7	1 6	bitr4i	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )