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

Definition df-t1 19581
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 19574 . 2  class  Fre
2 va . . . . . . 7  setvar  a
32cv 1378 . . . . . 6  class  a
43csn 4027 . . . . 5  class  { a }
5 vx . . . . . . 7  setvar  x
65cv 1378 . . . . . 6  class  x
7 ccld 19283 . . . . . 6  class  Clsd
86, 7cfv 5586 . . . . 5  class  ( Clsd `  x )
94, 8wcel 1767 . . . 4  wff  { a }  e.  ( Clsd `  x )
106cuni 4245 . . . 4  class  U. x
119, 2, 10wral 2814 . . 3  wff  A. a  e.  U. x { a }  e.  ( Clsd `  x )
12 ctop 19161 . . 3  class  Top
1311, 5, 12crab 2818 . 2  class  { x  e.  Top  |  A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
141, 13wceq 1379 1  wff  Fre  =  { x  e.  Top  | 
A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
Colors of variables: wff setvar class
This definition is referenced by:  ist1  19588
  Copyright terms: Public domain W3C validator