Definition df-2ndc 21243

Description: Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)

Assertion

Ref	Expression
df-2ndc	|- 2ndc = { j | E. x e. TopBases ( x ~<_ om /\ ( topGen ` x ) = j ) }

Distinct variable group:   x, j

Detailed syntax breakdown of Definition df-2ndc

Step	Hyp	Ref	Expression
1		c2ndc 21241	. 2 class 2ndc
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		ctg 16098	. . . . . . 7 class topGen
8	3, 7	cfv 5888	. . . . . 6 class ( topGen ` x )
9		vj	. . . . . . 7 setvar j
10	9	cv 1482	. . . . . 6 class j
11	8, 10	wceq 1483	. . . . 5 wff ( topGen ` x ) = j
12	6, 11	wa 384	. . . 4 wff ( x ~<_ om /\ ( topGen ` x ) = j )
13		ctb 20749	. . . 4 class TopBases
14	12, 2, 13	wrex 2913	. . 3 wff E. x e. TopBases ( x ~<_ om /\ ( topGen ` x ) = j )
15	14, 9	cab 2608	. 2 class { j | E. x e. TopBases ( x ~<_ om /\ ( topGen ` x ) = j ) }
16	1, 15	wceq 1483	1 wff 2ndc = { j | E. x e. TopBases ( x ~<_ om /\ ( topGen ` x ) = j ) }

This definition is referenced by:  is2ndc  21249