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

Definition df-nrm 21920
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 21913 . 2 class Nrm
2 vy . . . . . . . . 9 setvar 𝑦
32cv 1537 . . . . . . . 8 class 𝑦
4 vz . . . . . . . . 9 setvar 𝑧
54cv 1537 . . . . . . . 8 class 𝑧
63, 5wss 3919 . . . . . . 7 wff 𝑦𝑧
7 vj . . . . . . . . . . 11 setvar 𝑗
87cv 1537 . . . . . . . . . 10 class 𝑗
9 ccl 21621 . . . . . . . . . 10 class cls
108, 9cfv 6344 . . . . . . . . 9 class (cls‘𝑗)
115, 10cfv 6344 . . . . . . . 8 class ((cls‘𝑗)‘𝑧)
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1537 . . . . . . . 8 class 𝑥
1411, 13wss 3919 . . . . . . 7 wff ((cls‘𝑗)‘𝑧) ⊆ 𝑥
156, 14wa 399 . . . . . 6 wff (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
1615, 4, 8wrex 3134 . . . . 5 wff 𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
17 ccld 21619 . . . . . . 7 class Clsd
188, 17cfv 6344 . . . . . 6 class (Clsd‘𝑗)
1913cpw 4522 . . . . . 6 class 𝒫 𝑥
2018, 19cin 3918 . . . . 5 class ((Clsd‘𝑗) ∩ 𝒫 𝑥)
2116, 2, 20wral 3133 . . . 4 wff 𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
2221, 12, 8wral 3133 . . 3 wff 𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
23 ctop 21496 . . 3 class Top
2422, 7, 23crab 3137 . 2 class {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
251, 24wceq 1538 1 wff Nrm = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  isnrm  21938
  Copyright terms: Public domain W3C validator