df-reg

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)

		Ref	Expression
	Assertion	df-reg	$⊢ Reg = \{j \in Top \| \forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creg	$class Reg$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5		vy	$setvar y$
6	3	cv	$setvar x$
7		vz	$setvar z$
8	5	cv	$setvar y$
9	7	cv	$setvar z$
10	8 9	wcel	$wff y \in z$
11		ccl	$class cls$
12	4 11	cfv	$class cls (j)$
13	9 12	cfv	$class cls (j) (z)$
14	13 6	wss	$wff cls (j) (z) \subseteq x$
15	10 14	wa	$wff (y \in z \land cls (j) (z) \subseteq x)$
16	15 7 4	wrex	$wff \exists z \in j (y \in z \land cls (j) (z) \subseteq x)$
17	16 5 6	wral	$wff \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)$
18	17 3 4	wral	$wff \forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)$
19	18 1 2	crab	$class \{j \in Top \| \forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)\}$
20	0 19	wceq	$wff Reg = \{j \in Top \| \forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)\}$

Metamath Proof Explorer

Definition df-reg

Detailed syntax breakdown