Definition df-2ndc

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

	Ref	Expression
Assertion	df-2ndc	$$⊢2^{nd}𝜔=\left\{j|\exists x\in \mathrm{TopBases}\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left(x\right)=j\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2ndc	$$class{2}^{nd}𝜔$$
1		vj	$$setvarj$$
2		vx	$$setvarx$$
3		ctb	$$class\mathrm{TopBases}$$
4	2	cv	$$setvarx$$
5		cdom	$$class\preccurlyeq$$
6		com	$$class\mathrm{\omega }$$
7	4 6 5	wbr	$$wffx\preccurlyeq \mathrm{\omega }$$
8		ctg	$$class\mathrm{topGen}$$
9	4 8	cfv	$$class\mathrm{topGen}\left(x\right)$$
10	1	cv	$$setvarj$$
11	9 10	wceq	$$wff\mathrm{topGen}\left(x\right)=j$$
12	7 11	wa	$$wff\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left(x\right)=j\right)$$
13	12 2 3	wrex	$$wff\exists x\in \mathrm{TopBases}\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left(x\right)=j\right)$$
14	13 1	cab	$$class\left\{j|\exists x\in \mathrm{TopBases}\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left(x\right)=j\right)\right\}$$
15	0 14	wceq	$$wff{2}^{nd}𝜔=\left\{j|\exists x\in \mathrm{TopBases}\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left(x\right)=j\right)\right\}$$