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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creg	⊢ Reg
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5		vy	⊢ 𝑦
6	3	cv	⊢ 𝑥
7		vz	⊢ 𝑧
8	5	cv	⊢ 𝑦
9	7	cv	⊢ 𝑧
10	8 9	wcel	⊢ 𝑦 ∈ 𝑧
11		ccl	⊢ cls
12	4 11	cfv	⊢ ( cls ‘ 𝑗 )
13	9 12	cfv	⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑧 )
14	13 6	wss	⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥
15	10 14	wa	⊢ ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
16	15 7 4	wrex	⊢ ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
17	16 5 6	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
18	17 3 4	wral	⊢ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
19	18 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }
20	0 19	wceq	⊢ Reg = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑗 ( 𝑦 ∈ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }