# 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 ${⊢}\mathrm{Nrm}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrm ${class}\mathrm{Nrm}$
1 vj ${setvar}{j}$
2 ctop ${class}\mathrm{Top}$
3 vx ${setvar}{x}$
4 1 cv ${setvar}{j}$
5 vy ${setvar}{y}$
6 ccld ${class}\mathrm{Clsd}$
7 4 6 cfv ${class}\mathrm{Clsd}\left({j}\right)$
8 3 cv ${setvar}{x}$
9 8 cpw ${class}𝒫{x}$
10 7 9 cin ${class}\left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)$
11 vz ${setvar}{z}$
12 5 cv ${setvar}{y}$
13 11 cv ${setvar}{z}$
14 12 13 wss ${wff}{y}\subseteq {z}$
15 ccl ${class}\mathrm{cls}$
16 4 15 cfv ${class}\mathrm{cls}\left({j}\right)$
17 13 16 cfv ${class}\mathrm{cls}\left({j}\right)\left({z}\right)$
18 17 8 wss ${wff}\mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}$
19 14 18 wa ${wff}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)$
20 19 11 4 wrex ${wff}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)$
21 20 5 10 wral ${wff}\forall {y}\in \left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)$
22 21 3 4 wral ${wff}\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)$
23 22 1 2 crab ${class}\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)\right\}$
24 0 23 wceq ${wff}\mathrm{Nrm}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{Clsd}\left({j}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\exists {z}\in {j}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {z}\wedge \mathrm{cls}\left({j}\right)\left({z}\right)\subseteq {x}\right)\right\}$