Definition df-topsep

Description: A topology isseparable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015)

	Ref	Expression
Assertion	df-topsep	|- TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ _om /\ ( ( cls ` j ) ` x ) = U. j ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopsep	|- TopSep
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7	3	cv	|- x
8		cdom	|- ~<_
9		com	|- _om
10	7 9 8	wbr	|- x ~<_ _om
11		ccl	|- cls
12	4 11	cfv	|- ( cls ` j )
13	7 12	cfv	|- ( ( cls ` j ) ` x )
14	13 5	wceq	|- ( ( cls ` j ) ` x ) = U. j
15	10 14	wa	|- ( x ~<_ _om /\ ( ( cls ` j ) ` x ) = U. j )
16	15 3 6	wrex	|- E. x e. ~P U. j ( x ~<_ _om /\ ( ( cls ` j ) ` x ) = U. j )
17	16 1 2	crab	|- { j e. Top | E. x e. ~P U. j ( x ~<_ _om /\ ( ( cls ` j ) ` x ) = U. j ) }
18	0 17	wceq	|- TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ _om /\ ( ( cls ` j ) ` x ) = U. j ) }