Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nrm Structured version   Visualization version   GIF version

Definition df-nrm 21499
 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
StepHypRef Expression
1 cnrm 21492 . 2 class Nrm
2 vy . . . . . . . . 9 setvar 𝑦
32cv 1655 . . . . . . . 8 class 𝑦
4 vz . . . . . . . . 9 setvar 𝑧
54cv 1655 . . . . . . . 8 class 𝑧
63, 5wss 3798 . . . . . . 7 wff 𝑦𝑧
7 vj . . . . . . . . . . 11 setvar 𝑗
87cv 1655 . . . . . . . . . 10 class 𝑗
9 ccl 21200 . . . . . . . . . 10 class cls
108, 9cfv 6127 . . . . . . . . 9 class (cls‘𝑗)
115, 10cfv 6127 . . . . . . . 8 class ((cls‘𝑗)‘𝑧)
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1655 . . . . . . . 8 class 𝑥
1411, 13wss 3798 . . . . . . 7 wff ((cls‘𝑗)‘𝑧) ⊆ 𝑥
156, 14wa 386 . . . . . 6 wff (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
1615, 4, 8wrex 3118 . . . . 5 wff 𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
17 ccld 21198 . . . . . . 7 class Clsd
188, 17cfv 6127 . . . . . 6 class (Clsd‘𝑗)
1913cpw 4380 . . . . . 6 class 𝒫 𝑥
2018, 19cin 3797 . . . . 5 class ((Clsd‘𝑗) ∩ 𝒫 𝑥)
2116, 2, 20wral 3117 . . . 4 wff 𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
2221, 12, 8wral 3117 . . 3 wff 𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
23 ctop 21075 . . 3 class Top
2422, 7, 23crab 3121 . 2 class {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
251, 24wceq 1656 1 wff Nrm = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
 Colors of variables: wff setvar class This definition is referenced by:  isnrm  21517
 Copyright terms: Public domain W3C validator