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	$$⊢\mathrm{TopSep}=\left\{j\in \mathrm{Top}|\exists x\in 𝒫\bigcup j\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{cls}\left(j\right)\left(x\right)=\bigcup j\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopsep	$$class\mathrm{TopSep}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6	5	cpw	$$class𝒫\bigcup j$$
7	3	cv	$$setvarx$$
8		cdom	$$class\preccurlyeq$$
9		com	$$class\mathrm{\omega }$$
10	7 9 8	wbr	$$wffx\preccurlyeq \mathrm{\omega }$$
11		ccl	$$class\mathrm{cls}$$
12	4 11	cfv	$$class\mathrm{cls}\left(j\right)$$
13	7 12	cfv	$$class\mathrm{cls}\left(j\right)\left(x\right)$$
14	13 5	wceq	$$wff\mathrm{cls}\left(j\right)\left(x\right)=\bigcup j$$
15	10 14	wa	$$wff\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{cls}\left(j\right)\left(x\right)=\bigcup j\right)$$
16	15 3 6	wrex	$$wff\exists x\in 𝒫\bigcup j\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{cls}\left(j\right)\left(x\right)=\bigcup j\right)$$
17	16 1 2	crab	$$class\left\{j\in \mathrm{Top}|\exists x\in 𝒫\bigcup j\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{cls}\left(j\right)\left(x\right)=\bigcup j\right)\right\}$$
18	0 17	wceq	$$wff\mathrm{TopSep}=\left\{j\in \mathrm{Top}|\exists x\in 𝒫\bigcup j\left(x\preccurlyeq \mathrm{\omega }\wedge \mathrm{cls}\left(j\right)\left(x\right)=\bigcup j\right)\right\}$$