This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑗 ∈ 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 ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }