Metamath Proof Explorer

Definition df-nrm

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

Ref Expression
Assertion df-nrm ⊢ Nrm = j ∈ Top | ∀ x ∈ j ∀ y ∈ Clsd ⁡ j ∩ 𝒫 x ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrm class Nrm
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 vy setvar y
6 ccld class Clsd
7 4 6 cfv class Clsd ⁡ j
8 3 cv setvar x
9 8 cpw class 𝒫 x
10 7 9 cin class Clsd ⁡ j ∩ 𝒫 x
11 vz setvar z
12 5 cv setvar y
13 11 cv setvar z
14 12 13 wss wff y ⊆ z
15 ccl class cls
16 4 15 cfv class cls ⁡ j
17 13 16 cfv class cls ⁡ j ⁡ z
18 17 8 wss wff cls ⁡ j ⁡ z ⊆ x
19 14 18 wa wff y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x
20 19 11 4 wrex wff ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x
21 20 5 10 wral wff ∀ y ∈ Clsd ⁡ j ∩ 𝒫 x ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x
22 21 3 4 wral wff ∀ x ∈ j ∀ y ∈ Clsd ⁡ j ∩ 𝒫 x ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x
23 22 1 2 crab class j ∈ Top | ∀ x ∈ j ∀ y ∈ Clsd ⁡ j ∩ 𝒫 x ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x
24 0 23 wceq wff Nrm = j ∈ Top | ∀ x ∈ j ∀ y ∈ Clsd ⁡ j ∩ 𝒫 x ∃ z ∈ j y ⊆ z ∧ cls ⁡ j ⁡ z ⊆ x