MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-t1 Unicode version

Definition df-t1 17332
Description: The class of all T1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.)
Assertion
Ref Expression
df-t1  |-  Fre  =  { x  e.  Top  | 
A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
Distinct variable group:    x, a

Detailed syntax breakdown of Definition df-t1
StepHypRef Expression
1 ct1 17325 . 2  class  Fre
2 va . . . . . . 7  set  a
32cv 1648 . . . . . 6  class  a
43csn 3774 . . . . 5  class  { a }
5 vx . . . . . . 7  set  x
65cv 1648 . . . . . 6  class  x
7 ccld 17035 . . . . . 6  class  Clsd
86, 7cfv 5413 . . . . 5  class  ( Clsd `  x )
94, 8wcel 1721 . . . 4  wff  { a }  e.  ( Clsd `  x )
106cuni 3975 . . . 4  class  U. x
119, 2, 10wral 2666 . . 3  wff  A. a  e.  U. x { a }  e.  ( Clsd `  x )
12 ctop 16913 . . 3  class  Top
1311, 5, 12crab 2670 . 2  class  { x  e.  Top  |  A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
141, 13wceq 1649 1  wff  Fre  =  { x  e.  Top  | 
A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
Colors of variables: wff set class
This definition is referenced by:  ist1  17339
  Copyright terms: Public domain W3C validator