Definition df-reg 21120

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 21113	. 2 class Reg
2		vy	. . . . . . . 8 setvar y
3		vz	. . . . . . . 8 setvar z
4	2, 3	wel 1991	. . . . . . 7 wff y e. z
5	3	cv 1482	. . . . . . . . 9 class z
6		vj	. . . . . . . . . . 11 setvar j
7	6	cv 1482	. . . . . . . . . 10 class j
8		ccl 20822	. . . . . . . . . 10 class cls
9	7, 8	cfv 5888	. . . . . . . . 9 class ( cls ` j )
10	5, 9	cfv 5888	. . . . . . . 8 class ( ( cls ` j ) ` z )
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1482	. . . . . . . 8 class x
13	10, 12	wss 3574	. . . . . . 7 wff ( ( cls ` j ) ` z ) C_ x
14	4, 13	wa 384	. . . . . 6 wff ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
15	14, 3, 7	wrex 2913	. . . . 5 wff E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
16	15, 2, 12	wral 2912	. . . 4 wff A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
17	16, 11, 7	wral 2912	. . 3 wff A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
18		ctop 20698	. . 3 class Top
19	17, 6, 18	crab 2916	. 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 1483	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  21136