Metamath Proof Explorer

Theorem elflim

Description: The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion elflim ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ F

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 1 adantr ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → J ∈ Top
3 fvssunirn ⊢ Fil ⁡ X ⊆ ⋃ ran ⁡ Fil
4 3 sseli ⊢ F ∈ Fil ⁡ X → F ∈ ⋃ ran ⁡ Fil
5 4 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → F ∈ ⋃ ran ⁡ Fil
6 filsspw ⊢ F ∈ Fil ⁡ X → F ⊆ 𝒫 X
7 6 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → F ⊆ 𝒫 X
8 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
9 8 adantr ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → X = ⋃ J
10 9 pweqd ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → 𝒫 X = 𝒫 ⋃ J
11 7 10 sseqtrd ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → F ⊆ 𝒫 ⋃ J
12 eqid ⊢ ⋃ J = ⋃ J
13 12 elflim2 ⊢ A ∈ J fLim F ↔ J ∈ Top ∧ F ∈ ⋃ ran ⁡ Fil ∧ F ⊆ 𝒫 ⋃ J ∧ A ∈ ⋃ J ∧ nei ⁡ J ⁡ A ⊆ F
14 13 baib ⊢ J ∈ Top ∧ F ∈ ⋃ ran ⁡ Fil ∧ F ⊆ 𝒫 ⋃ J → A ∈ J fLim F ↔ A ∈ ⋃ J ∧ nei ⁡ J ⁡ A ⊆ F
15 2 5 11 14 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fLim F ↔ A ∈ ⋃ J ∧ nei ⁡ J ⁡ A ⊆ F
16 9 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ X ↔ A ∈ ⋃ J
17 16 anbi1d ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ X ∧ nei ⁡ J ⁡ A ⊆ F ↔ A ∈ ⋃ J ∧ nei ⁡ J ⁡ A ⊆ F
18 15 17 bitr4d ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fLim F ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ F