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

Metamath Proof Explorer

Definition df-nrm

Description: Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion df-nrm Nrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrm ⊢ Nrm
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑗
5 vy ⊢ 𝑦
6 ccld ⊢ Clsd
7 4 6 cfv ⊢ ( Clsd ‘ 𝑗 )
8 3 cv ⊢ 𝑥
9 8 cpw ⊢ 𝒫 𝑥
10 7 9 cin ⊢ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 )
11 vz ⊢ 𝑧
12 5 cv ⊢ 𝑦
13 11 cv ⊢ 𝑧
14 12 13 wss ⊢ 𝑦 ⊆ 𝑧
15 ccl ⊢ cls
16 4 15 cfv ⊢ ( cls ‘ 𝑗 )
17 13 16 cfv ⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑧 )
18 17 8 wss ⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥
19 14 18 wa ⊢ ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
20 19 11 4 wrex ⊢ ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
21 20 5 10 wral ⊢ ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
22 21 3 4 wral ⊢ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 )
23 22 1 2 crab ⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }
24 0 23 wceq ⊢ Nrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝑗 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝑗 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑧 ) ⊆ 𝑥 ) }