Metamath Proof Explorer

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 = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ 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 ∈ 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 ⊆ x
15 10 14 wa wff y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x
16 15 7 4 wrex wff ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x
17 16 5 6 wral wff ∀ y ∈ x ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x
18 17 3 4 wral wff ∀ x ∈ j ∀ y ∈ x ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x
19 18 1 2 crab class j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x
20 0 19 wceq wff Reg = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ z ∈ j y ∈ z ∧ cls ⁡ j ⁡ z ⊆ x