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

Definition df-t1 18877
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 18870 . 2  class  Fre
2 va . . . . . . 7  setvar  a
32cv 1363 . . . . . 6  class  a
43csn 3874 . . . . 5  class  { a }
5 vx . . . . . . 7  setvar  x
65cv 1363 . . . . . 6  class  x
7 ccld 18579 . . . . . 6  class  Clsd
86, 7cfv 5415 . . . . 5  class  ( Clsd `  x )
94, 8wcel 1761 . . . 4  wff  { a }  e.  ( Clsd `  x )
106cuni 4088 . . . 4  class  U. x
119, 2, 10wral 2713 . . 3  wff  A. a  e.  U. x { a }  e.  ( Clsd `  x )
12 ctop 18457 . . 3  class  Top
1311, 5, 12crab 2717 . 2  class  { x  e.  Top  |  A. a  e.  U. x { a }  e.  ( Clsd `  x ) }
141, 13wceq 1364 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  18884
  Copyright terms: Public domain W3C validator