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

Definition df-t1 17042
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 17035 . 2  class  Fre
2 va . . . . . . 7  set  a
32cv 1622 . . . . . 6  class  a
43csn 3640 . . . . 5  class  { a }
5 vx . . . . . . 7  set  x
65cv 1622 . . . . . 6  class  x
7 ccld 16753 . . . . . 6  class  Clsd
86, 7cfv 5255 . . . . 5  class  ( Clsd `  x )
94, 8wcel 1684 . . . 4  wff  { a }  e.  ( Clsd `  x )
106cuni 3827 . . . 4  class  U. x
119, 2, 10wral 2543 . . 3  wff  A. a  e.  U. x { a }  e.  ( Clsd `  x )
12 ctop 16631 . . 3  class  Top
1311, 5, 12crab 2547 . 2  class  { x  e.  Top  |  A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
141, 13wceq 1623 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  17049
  Copyright terms: Public domain W3C validator