Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fclsval Structured version   Unicode version

Theorem fclsval 20487
 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.)
Hypothesis
Ref Expression
fclsval.x
Assertion
Ref Expression
fclsval
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem fclsval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . 3
2 fvssunirn 5879 . . . . 5
32sseli 3485 . . . 4
5 filn0 20341 . . . . . 6
65adantl 466 . . . . 5
7 fvex 5866 . . . . . 6
87rgenw 2804 . . . . 5
9 iinexg 4597 . . . . 5
106, 8, 9sylancl 662 . . . 4
11 0ex 4567 . . . 4
12 ifcl 3968 . . . 4
1310, 11, 12sylancl 662 . . 3
14 unieq 4242 . . . . . . 7
15 fclsval.x . . . . . . 7
1614, 15syl6eqr 2502 . . . . . 6
17 unieq 4242 . . . . . 6
1816, 17eqeqan12d 2466 . . . . 5
19 iineq1 4330 . . . . . . 7
2019adantl 466 . . . . . 6
21 simpll 753 . . . . . . . . 9
2221fveq2d 5860 . . . . . . . 8
2322fveq1d 5858 . . . . . . 7
2423iineq2dv 4338 . . . . . 6
2520, 24eqtrd 2484 . . . . 5
2618, 25ifbieq1d 3949 . . . 4
27 df-fcls 20420 . . . 4
2826, 27ovmpt2ga 6417 . . 3
291, 4, 13, 28syl3anc 1229 . 2
30 filunibas 20360 . . . . 5
3130eqeq2d 2457 . . . 4