Definition df-nrm 21121

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 = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }

Distinct variable group:   x, j, y, z

Detailed syntax breakdown of Definition df-nrm

Step	Hyp	Ref	Expression
1		cnrm 21114	. 2 class Nrm
2		vy	. . . . . . . . 9 setvar y
3	2	cv 1482	. . . . . . . 8 class y
4		vz	. . . . . . . . 9 setvar z
5	4	cv 1482	. . . . . . . 8 class z
6	3, 5	wss 3574	. . . . . . 7 wff y C_ z
7		vj	. . . . . . . . . . 11 setvar j
8	7	cv 1482	. . . . . . . . . 10 class j
9		ccl 20822	. . . . . . . . . 10 class cls
10	8, 9	cfv 5888	. . . . . . . . 9 class ( cls ` j )
11	5, 10	cfv 5888	. . . . . . . 8 class ( ( cls ` j ) ` z )
12		vx	. . . . . . . . 9 setvar x
13	12	cv 1482	. . . . . . . 8 class x
14	11, 13	wss 3574	. . . . . . 7 wff ( ( cls ` j ) ` z ) C_ x
15	6, 14	wa 384	. . . . . 6 wff ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
16	15, 4, 8	wrex 2913	. . . . 5 wff E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
17		ccld 20820	. . . . . . 7 class Clsd
18	8, 17	cfv 5888	. . . . . 6 class ( Clsd ` j )
19	13	cpw 4158	. . . . . 6 class ~P x
20	18, 19	cin 3573	. . . . 5 class ( ( Clsd ` j ) i^i ~P x )
21	16, 2, 20	wral 2912	. . . 4 wff A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
22	21, 12, 8	wral 2912	. . 3 wff A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
23		ctop 20698	. . 3 class Top
24	22, 7, 23	crab 2916	. 2 class { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }
25	1, 24	wceq 1483	1 wff Nrm = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }

This definition is referenced by:  isnrm  21139