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

Metamath Proof Explorer

Definition df-t1

Description: The class of all T_1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007)

Ref Expression
Assertion df-t1 
|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ct1 
 |-  Fre
1 vx 
 |-  x
2 ctop 
 |-  Top
3 va 
 |-  a
4 1 cv 
 |-  x
5 4 cuni 
 |-  U. x
6 3 cv 
 |-  a
7 6 csn 
 |-  { a }
8 ccld 
 |-  Clsd
9 4 8 cfv 
 |-  ( Clsd ` x )
10 7 9 wcel 
 |-  { a } e. ( Clsd ` x )
11 10 3 5 wral 
 |-  A. a e. U. x { a } e. ( Clsd ` x )
12 11 1 2 crab 
 |-  { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
13 0 12 wceq 
 |-  Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }