Theorem dfnrm2

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

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

Proof

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