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