Definition df-2ndc

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2ndc	|- 2ndc
1		vj	|- j
2		vx	|- x
3		ctb	|- TopBases
4	2	cv	|- x
5		cdom	|- ~<_
6		com	|- _om
7	4 6 5	wbr	|- x ~<_ _om
8		ctg	|- topGen
9	4 8	cfv	|- ( topGen ` x )
10	1	cv	|- j
11	9 10	wceq	|- ( topGen ` x ) = j
12	7 11	wa	|- ( x ~<_ _om /\ ( topGen ` x ) = j )
13	12 2 3	wrex	|- E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j )
14	13 1	cab	|- { j | E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) }
15	0 14	wceq	|- 2ndc = { j | E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = j ) }