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	⊢ TopSep = { 𝑗 ∈ Top ∣ ∃ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopsep	⊢ TopSep
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6	5	cpw	⊢ 𝒫 ∪ 𝑗
7	3	cv	⊢ 𝑥
8		cdom	⊢ ≼
9		com	⊢ ω
10	7 9 8	wbr	⊢ 𝑥 ≼ ω
11		ccl	⊢ cls
12	4 11	cfv	⊢ ( cls ‘ 𝑗 )
13	7 12	cfv	⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑥 )
14	13 5	wceq	⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗
15	10 14	wa	⊢ ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗 )
16	15 3 6	wrex	⊢ ∃ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗 )
17	16 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ∃ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗 ) }
18	0 17	wceq	⊢ TopSep = { 𝑗 ∈ Top ∣ ∃ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) = ∪ 𝑗 ) }