Description: Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | flimcls | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | flimclslem | |
3 | 3anass | |
|
4 | 2 3 | sylib | |
5 | eleq2 | |
|
6 | oveq2 | |
|
7 | 6 | eleq2d | |
8 | 5 7 | anbi12d | |
9 | 8 | rspcev | |
10 | 4 9 | syl | |
11 | 10 | 3expia | |
12 | flimclsi | |
|
13 | 12 | sselda | |
14 | 13 | rexlimivw | |
15 | 11 14 | impbid1 | |