Definition df-reg 19038

Description: Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)

Assertion

Ref	Expression
df-reg	|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }

Distinct variable group:   x, j, y, z

Detailed syntax breakdown of Definition df-reg

Step	Hyp	Ref	Expression
1		creg 19031	. 2 class Reg
2		vy	. . . . . . . 8 setvar y
3		vz	. . . . . . . 8 setvar z
4	2, 3	wel 1759	. . . . . . 7 wff y e. z
5	3	cv 1369	. . . . . . . . 9 class z
6		vj	. . . . . . . . . . 11 setvar j
7	6	cv 1369	. . . . . . . . . 10 class j
8		ccl 18740	. . . . . . . . . 10 class cls
9	7, 8	cfv 5518	. . . . . . . . 9 class ( cls ` j )
10	5, 9	cfv 5518	. . . . . . . 8 class ( ( cls ` j ) ` z )
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1369	. . . . . . . 8 class x
13	10, 12	wss 3428	. . . . . . 7 wff ( ( cls ` j ) ` z ) C_ x
14	4, 13	wa 369	. . . . . 6 wff ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
15	14, 3, 7	wrex 2796	. . . . 5 wff E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
16	15, 2, 12	wral 2795	. . . 4 wff A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
17	16, 11, 7	wral 2795	. . 3 wff A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
18		ctop 18616	. . 3 class Top
19	17, 6, 18	crab 2799	. 2 class { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }
20	1, 19	wceq 1370	1 wff Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }

This definition is referenced by:  isreg  19054