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 \in Top \| \forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq 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) \cap 𝒫 x)$
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 cls$
16	4 15	cfv	$class cls (j)$
17	13 16	cfv	$class cls (j) (z)$
18	17 8	wss	$wff cls (j) (z) \subseteq x$
19	14 18	wa	$wff (y \subseteq z \land cls (j) (z) \subseteq x)$
20	19 11 4	wrex	$wff \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)$
21	20 5 10	wral	$wff \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)$
22	21 3 4	wral	$wff \forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)$
23	22 1 2	crab	$class \{j \in Top \| \forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)\}$
24	0 23	wceq	$wff Nrm = \{j \in Top \| \forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)\}$

Metamath Proof Explorer

Definition df-nrm

Detailed syntax breakdown