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

Theorem fclsval 18040
 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 444 . . 3
2 fvssunirn 5754 . . . . 5
32sseli 3344 . . . 4
5 filn0 17894 . . . . . 6
65adantl 453 . . . . 5
7 fvex 5742 . . . . . 6
87rgenw 2773 . . . . 5
9 iinexg 4360 . . . . 5
106, 8, 9sylancl 644 . . . 4
11 0ex 4339 . . . 4
12 ifcl 3775 . . . 4
1310, 11, 12sylancl 644 . . 3
14 unieq 4024 . . . . . . 7
15 fclsval.x . . . . . . 7
1614, 15syl6eqr 2486 . . . . . 6
17 unieq 4024 . . . . . 6
1816, 17eqeqan12d 2451 . . . . 5
19 iineq1 4107 . . . . . . 7
2019adantl 453 . . . . . 6
21 simpll 731 . . . . . . . . 9
2221fveq2d 5732 . . . . . . . 8
2322fveq1d 5730 . . . . . . 7
2423iineq2dv 4115 . . . . . 6
2520, 24eqtrd 2468 . . . . 5
26 eqidd 2437 . . . . 5
2718, 25, 26ifbieq12d 3761 . . . 4
28 df-fcls 17973 . . . 4
2927, 28ovmpt2ga 6203 . . 3
301, 4, 13, 29syl3anc 1184 . 2
31 filunibas 17913 . . . . 5
3231eqeq2d 2447 . . . 4