Definition df-reg 21927

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 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}

Distinct variable group:   𝑥,𝑗,𝑦,𝑧

Detailed syntax breakdown of Definition df-reg

Step	Hyp	Ref	Expression
1		creg 21920	. 2 class Reg
2		vy	. . . . . . . 8 setvar 𝑦
3		vz	. . . . . . . 8 setvar 𝑧
4	2, 3	wel 2114	. . . . . . 7 wff 𝑦 ∈ 𝑧
5	3	cv 1535	. . . . . . . . 9 class 𝑧
6		vj	. . . . . . . . . . 11 setvar 𝑗
7	6	cv 1535	. . . . . . . . . 10 class 𝑗
8		ccl 21629	. . . . . . . . . 10 class cls
9	7, 8	cfv 6358	. . . . . . . . 9 class (cls‘𝑗)
10	5, 9	cfv 6358	. . . . . . . 8 class ((cls‘𝑗)‘𝑧)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1535	. . . . . . . 8 class 𝑥
13	10, 12	wss 3939	. . . . . . 7 wff ((cls‘𝑗)‘𝑧) ⊆ 𝑥
14	4, 13	wa 398	. . . . . 6 wff (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
15	14, 3, 7	wrex 3142	. . . . 5 wff ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
16	15, 2, 12	wral 3141	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
17	16, 11, 7	wral 3141	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)
18		ctop 21504	. . 3 class Top
19	17, 6, 18	crab 3145	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
20	1, 19	wceq 1536	1 wff Reg = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}

This definition is referenced by:  isreg  21943