Metamath Proof Explorer


Theorem fclsval

Description: The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis fclsval.x X = J
Assertion fclsval J Top F Fil Y J fClus F = if X = Y t F cls J t

Proof

Step Hyp Ref Expression
1 fclsval.x X = J
2 simpl J Top F Fil Y J Top
3 fvssunirn Fil Y ran Fil
4 3 sseli F Fil Y F ran Fil
5 4 adantl J Top F Fil Y F ran Fil
6 filn0 F Fil Y F
7 6 adantl J Top F Fil Y F
8 fvex cls J t V
9 8 rgenw t F cls J t V
10 iinexg F t F cls J t V t F cls J t V
11 7 9 10 sylancl J Top F Fil Y t F cls J t V
12 0ex V
13 ifcl t F cls J t V V if X = F t F cls J t V
14 11 12 13 sylancl J Top F Fil Y if X = F t F cls J t V
15 unieq j = J j = J
16 15 1 eqtr4di j = J j = X
17 unieq f = F f = F
18 16 17 eqeqan12d j = J f = F j = f X = F
19 iineq1 f = F t f cls j t = t F cls j t
20 19 adantl j = J f = F t f cls j t = t F cls j t
21 simpll j = J f = F t F j = J
22 21 fveq2d j = J f = F t F cls j = cls J
23 22 fveq1d j = J f = F t F cls j t = cls J t
24 23 iineq2dv j = J f = F t F cls j t = t F cls J t
25 20 24 eqtrd j = J f = F t f cls j t = t F cls J t
26 18 25 ifbieq1d j = J f = F if j = f t f cls j t = if X = F t F cls J t
27 df-fcls fClus = j Top , f ran Fil if j = f t f cls j t
28 26 27 ovmpoga J Top F ran Fil if X = F t F cls J t V J fClus F = if X = F t F cls J t
29 2 5 14 28 syl3anc J Top F Fil Y J fClus F = if X = F t F cls J t
30 filunibas F Fil Y F = Y
31 30 eqeq2d F Fil Y X = F X = Y
32 31 adantl J Top F Fil Y X = F X = Y
33 32 ifbid J Top F Fil Y if X = F t F cls J t = if X = Y t F cls J t
34 29 33 eqtrd J Top F Fil Y J fClus F = if X = Y t F cls J t