Definition df-fcls 23000

Description: Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.)

Assertion

Ref	Expression
df-fcls	⊢ fClus = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))

Distinct variable group:   𝑓,𝑗,𝑥

Detailed syntax breakdown of Definition df-fcls

Step	Hyp	Ref	Expression
1		cfcls 22995	. 2 class fClus
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 21950	. . 3 class Top
5		cfil 22904	. . . . 5 class Fil
6	5	crn 5581	. . . 4 class ran Fil
7	6	cuni 4836	. . 3 class ∪ ran Fil
8	2	cv 1538	. . . . . 6 class 𝑗
9	8	cuni 4836	. . . . 5 class ∪ 𝑗
10	3	cv 1538	. . . . . 6 class 𝑓
11	10	cuni 4836	. . . . 5 class ∪ 𝑓
12	9, 11	wceq 1539	. . . 4 wff ∪ 𝑗 = ∪ 𝑓
13		vx	. . . . 5 setvar 𝑥
14	13	cv 1538	. . . . . 6 class 𝑥
15		ccl 22077	. . . . . . 7 class cls
16	8, 15	cfv 6418	. . . . . 6 class (cls‘𝑗)
17	14, 16	cfv 6418	. . . . 5 class ((cls‘𝑗)‘𝑥)
18	13, 10, 17	ciin 4922	. . . 4 class ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥)
19		c0 4253	. . . 4 class ∅
20	12, 18, 19	cif 4456	. . 3 class if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)
21	2, 3, 4, 7, 20	cmpo 7257	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))
22	1, 21	wceq 1539	1 wff fClus = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))

This definition is referenced by:  fclsval  23067  isfcls  23068