Theorem dfnrm3

Description: A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm . (Contributed by Zhi Wang, 2-Sep-2024)

	Ref	Expression
Assertion	dfnrm3	⊢ Nrm = { 𝑗 ∈ Top ∣ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) }

Proof

Step	Hyp	Ref	Expression
1		isnrm4	⊢ ( 𝑗 ∈ Nrm ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
2	1	eqabi	⊢ Nrm = { 𝑗 ∣ ( 𝑗 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) }
3		df-rab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) } = { 𝑗 ∣ ( 𝑗 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) }
4	2 3	eqtr4i	⊢ Nrm = { 𝑗 ∈ Top ∣ ∀ 𝑐 ∈ ( Clsd ‘ 𝑗 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝑗 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑐 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝑗 ) ‘ 𝑑 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) }