Metamath Proof Explorer


Theorem flimval

Description: The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimval.1 X = J
Assertion flimval J Top F ran Fil J fLim F = x X | nei J x F F 𝒫 X

Proof

Step Hyp Ref Expression
1 flimval.1 X = J
2 1 topopn J Top X J
3 2 adantr J Top F ran Fil X J
4 rabexg X J x X | nei J x F F 𝒫 X V
5 3 4 syl J Top F ran Fil x X | nei J x F F 𝒫 X V
6 simpl j = J f = F j = J
7 6 unieqd j = J f = F j = J
8 7 1 eqtr4di j = J f = F j = X
9 6 fveq2d j = J f = F nei j = nei J
10 9 fveq1d j = J f = F nei j x = nei J x
11 simpr j = J f = F f = F
12 10 11 sseq12d j = J f = F nei j x f nei J x F
13 8 pweqd j = J f = F 𝒫 j = 𝒫 X
14 11 13 sseq12d j = J f = F f 𝒫 j F 𝒫 X
15 12 14 anbi12d j = J f = F nei j x f f 𝒫 j nei J x F F 𝒫 X
16 8 15 rabeqbidv j = J f = F x j | nei j x f f 𝒫 j = x X | nei J x F F 𝒫 X
17 df-flim fLim = j Top , f ran Fil x j | nei j x f f 𝒫 j
18 16 17 ovmpoga J Top F ran Fil x X | nei J x F F 𝒫 X V J fLim F = x X | nei J x F F 𝒫 X
19 5 18 mpd3an3 J Top F ran Fil J fLim F = x X | nei J x F F 𝒫 X