Definition df-fcls 22546

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 22541	. 2 class fClus
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 21498	. . 3 class Top
5		cfil 22450	. . . . 5 class Fil
6	5	crn 5520	. . . 4 class ran Fil
7	6	cuni 4800	. . 3 class ∪ ran Fil
8	2	cv 1537	. . . . . 6 class 𝑗
9	8	cuni 4800	. . . . 5 class ∪ 𝑗
10	3	cv 1537	. . . . . 6 class 𝑓
11	10	cuni 4800	. . . . 5 class ∪ 𝑓
12	9, 11	wceq 1538	. . . 4 wff ∪ 𝑗 = ∪ 𝑓
13		vx	. . . . 5 setvar 𝑥
14	13	cv 1537	. . . . . 6 class 𝑥
15		ccl 21623	. . . . . . 7 class cls
16	8, 15	cfv 6324	. . . . . 6 class (cls‘𝑗)
17	14, 16	cfv 6324	. . . . 5 class ((cls‘𝑗)‘𝑥)
18	13, 10, 17	ciin 4882	. . . 4 class ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥)
19		c0 4243	. . . 4 class ∅
20	12, 18, 19	cif 4425	. . 3 class if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)
21	2, 3, 4, 7, 20	cmpo 7137	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))
22	1, 21	wceq 1538	1 wff fClus = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))

This definition is referenced by:  fclsval  22613  isfcls  22614