Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-topsep Unicode version

Definition df-topsep 27637
Description: A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
Assertion
Ref Expression
df-topsep  |- TopSep  =  {
j  e.  Top  |  E. x  e.  ~P  U. j ( x  ~<_  om 
/\  ( ( cls `  j ) `  x
)  =  U. j
) }
Distinct variable group:    x, j

Detailed syntax breakdown of Definition df-topsep
StepHypRef Expression
1 ctopsep 27635 . 2  class TopSep
2 vx . . . . . . 7  set  x
32cv 1631 . . . . . 6  class  x
4 com 4672 . . . . . 6  class  om
5 cdom 6877 . . . . . 6  class  ~<_
63, 4, 5wbr 4039 . . . . 5  wff  x  ~<_  om
7 vj . . . . . . . . 9  set  j
87cv 1631 . . . . . . . 8  class  j
9 ccl 16771 . . . . . . . 8  class  cls
108, 9cfv 5271 . . . . . . 7  class  ( cls `  j )
113, 10cfv 5271 . . . . . 6  class  ( ( cls `  j ) `
 x )
128cuni 3843 . . . . . 6  class  U. j
1311, 12wceq 1632 . . . . 5  wff  ( ( cls `  j ) `
 x )  = 
U. j
146, 13wa 358 . . . 4  wff  ( x  ~<_  om  /\  ( ( cls `  j ) `
 x )  = 
U. j )
1512cpw 3638 . . . 4  class  ~P U. j
1614, 2, 15wrex 2557 . . 3  wff  E. x  e.  ~P  U. j ( x  ~<_  om  /\  (
( cls `  j
) `  x )  =  U. j )
17 ctop 16647 . . 3  class  Top
1816, 7, 17crab 2560 . 2  class  { j  e.  Top  |  E. x  e.  ~P  U. j
( x  ~<_  om  /\  ( ( cls `  j
) `  x )  =  U. j ) }
191, 18wceq 1632 1  wff TopSep  =  {
j  e.  Top  |  E. x  e.  ~P  U. j ( x  ~<_  om 
/\  ( ( cls `  j ) `  x
)  =  U. j
) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator