Definition df-topsep 37793

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

Step	Hyp	Ref	Expression
1		ctopsep 37791	. 2 class TopSep
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		com 7065	. . . . . 6 class om
5		cdom 7953	. . . . . 6 class ~<_
6	3, 4, 5	wbr 4653	. . . . 5 wff x ~<_ om
7		vj	. . . . . . . . 9 setvar j
8	7	cv 1482	. . . . . . . 8 class j
9		ccl 20822	. . . . . . . 8 class cls
10	8, 9	cfv 5888	. . . . . . 7 class ( cls ` j )
11	3, 10	cfv 5888	. . . . . 6 class ( ( cls ` j ) ` x )
12	8	cuni 4436	. . . . . 6 class U. j
13	11, 12	wceq 1483	. . . . 5 wff ( ( cls ` j ) ` x ) = U. j
14	6, 13	wa 384	. . . 4 wff ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j )
15	12	cpw 4158	. . . 4 class ~P U. j
16	14, 2, 15	wrex 2913	. . 3 wff E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j )
17		ctop 20698	. . 3 class Top
18	16, 7, 17	crab 2916	. 2 class { j e. Top | E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j ) }
19	1, 18	wceq 1483	1 wff TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j ) }

This definition is referenced by: (None)