Definition df-nrm 23647

Description: Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)

Assertion

Ref	Expression
df-nrm	⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}

Distinct variable group:   𝑥,𝑗,𝑦,𝑧

Detailed syntax breakdown of Definition df-nrm

Step	Hyp	Ref	Expression
1		cnrm 23640	. 2 class Nrm
2		vy	. . . . . . . . 9 setvar 𝑦
3	2	cv 1568	. . . . . . . 8 class 𝑦
4		vz	. . . . . . . . 9 setvar 𝑧
5	4	cv 1568	. . . . . . . 8 class 𝑧
6	3, 5	wss 3899	. . . . . . 7 wff 𝑦 ⊆ 𝑧
7		vj	. . . . . . . . . . 11 setvar 𝑗
8	7	cv 1568	. . . . . . . . . 10 class 𝑗
9		ccl 23348	. . . . . . . . . 10 class cls
10	8, 9	cfv 6546	. . . . . . . . 9 class (cls‘𝑗)
11	5, 10	cfv 6546	. . . . . . . 8 class ((cls‘𝑗)‘𝑧)
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1568	. . . . . . . 8 class 𝑥
14	11, 13	wss 3899	. . . . . . 7 wff ((cls‘𝑗)‘𝑧) ⊆ 𝑥
15	6, 14	wa 401	. . . . . 6 wff (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
16	15, 4, 8	wrex 3089	. . . . 5 wff ∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
17		ccld 23346	. . . . . . 7 class Clsd
18	8, 17	cfv 6546	. . . . . 6 class (Clsd‘𝑗)
19	13	cpw 4559	. . . . . 6 class 𝒫 𝑥
20	18, 19	cin 4091	. . . . 5 class ((Clsd‘𝑗) ∩ 𝒫 𝑥)
21	16, 2, 20	wral 3079	. . . 4 wff ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
22	21, 12, 8	wral 3079	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
23		ctop 23223	. . 3 class Top
24	22, 7, 23	crab 3415	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
25	1, 24	wceq 1569	1 wff Nrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}

This definition is used by:  isnrm  23665