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 = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrm 
 |-  Nrm
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vx 
 |-  x
4 1 cv 
 |-  j
5 vy 
 |-  y
6 ccld 
 |-  Clsd
7 4 6 cfv 
 |-  ( Clsd ` j )
8 3 cv 
 |-  x
9 8 cpw 
 |-  ~P x
10 7 9 cin 
 |-  ( ( Clsd ` j ) i^i ~P x )
11 vz 
 |-  z
12 5 cv 
 |-  y
13 11 cv 
 |-  z
14 12 13 wss 
 |-  y C_ z
15 ccl 
 |-  cls
16 4 15 cfv 
 |-  ( cls ` j )
17 13 16 cfv 
 |-  ( ( cls ` j ) ` z )
18 17 8 wss 
 |-  ( ( cls ` j ) ` z ) C_ x
19 14 18 wa 
 |-  ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
20 19 11 4 wrex 
 |-  E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
21 20 5 10 wral 
 |-  A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
22 21 3 4 wral 
 |-  A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x )
23 22 1 2 crab 
 |-  { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }
24 0 23 wceq 
 |-  Nrm = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }