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