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 21853
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 21846 . 2 class Nrm
2 vy . . . . . . . . 9 setvar 𝑦
32cv 1527 . . . . . . . 8 class 𝑦
4 vz . . . . . . . . 9 setvar 𝑧
54cv 1527 . . . . . . . 8 class 𝑧
63, 5wss 3933 . . . . . . 7 wff 𝑦𝑧
7 vj . . . . . . . . . . 11 setvar 𝑗
87cv 1527 . . . . . . . . . 10 class 𝑗
9 ccl 21554 . . . . . . . . . 10 class cls
108, 9cfv 6348 . . . . . . . . 9 class (cls‘𝑗)
115, 10cfv 6348 . . . . . . . 8 class ((cls‘𝑗)‘𝑧)
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1527 . . . . . . . 8 class 𝑥
1411, 13wss 3933 . . . . . . 7 wff ((cls‘𝑗)‘𝑧) ⊆ 𝑥
156, 14wa 396 . . . . . 6 wff (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
1615, 4, 8wrex 3136 . . . . 5 wff 𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
17 ccld 21552 . . . . . . 7 class Clsd
188, 17cfv 6348 . . . . . 6 class (Clsd‘𝑗)
1913cpw 4535 . . . . . 6 class 𝒫 𝑥
2018, 19cin 3932 . . . . 5 class ((Clsd‘𝑗) ∩ 𝒫 𝑥)
2116, 2, 20wral 3135 . . . 4 wff 𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
2221, 12, 8wral 3135 . . 3 wff 𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
23 ctop 21429 . . 3 class Top
2422, 7, 23crab 3139 . 2 class {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
251, 24wceq 1528 1 wff Nrm = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧𝑗 (𝑦𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  isnrm  21871
  Copyright terms: Public domain W3C validator