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	$⊢ TopSep = \{j \in Top \| \exists x \in 𝒫 ⋃ j (x ≼ ω \land cls (j) (x) = ⋃ j)\}$

Step	Hyp	Ref	Expression
0		ctopsep	$class TopSep$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6	5	cpw	$class 𝒫 ⋃ j$
7	3	cv	$setvar x$
8		cdom	$class ≼$
9		com	$class ω$
10	7 9 8	wbr	$wff x ≼ ω$
11		ccl	$class cls$
12	4 11	cfv	$class cls (j)$
13	7 12	cfv	$class cls (j) (x)$
14	13 5	wceq	$wff cls (j) (x) = ⋃ j$
15	10 14	wa	$wff (x ≼ ω \land cls (j) (x) = ⋃ j)$
16	15 3 6	wrex	$wff \exists x \in 𝒫 ⋃ j (x ≼ ω \land cls (j) (x) = ⋃ j)$
17	16 1 2	crab	$class \{j \in Top \| \exists x \in 𝒫 ⋃ j (x ≼ ω \land cls (j) (x) = ⋃ j)\}$
18	0 17	wceq	$wff TopSep = \{j \in Top \| \exists x \in 𝒫 ⋃ j (x ≼ ω \land cls (j) (x) = ⋃ j)\}$

Metamath Proof Explorer