Metamath Proof Explorer

Theorem isfcls2

Description: A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isfcls2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
3 2 fveq2d ⊢ J ∈ TopOn ⁡ X → Fil ⁡ X = Fil ⁡ ⋃ J
4 3 eleq2d ⊢ J ∈ TopOn ⁡ X → F ∈ Fil ⁡ X ↔ F ∈ Fil ⁡ ⋃ J
5 4 biimpa ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → F ∈ Fil ⁡ ⋃ J
6 eqid ⊢ ⋃ J = ⋃ J
7 6 isfcls ⊢ A ∈ J fClus F ↔ J ∈ Top ∧ F ∈ Fil ⁡ ⋃ J ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s
8 df-3an ⊢ J ∈ Top ∧ F ∈ Fil ⁡ ⋃ J ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s ↔ J ∈ Top ∧ F ∈ Fil ⁡ ⋃ J ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s
9 7 8 bitri ⊢ A ∈ J fClus F ↔ J ∈ Top ∧ F ∈ Fil ⁡ ⋃ J ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s
10 9 baib ⊢ J ∈ Top ∧ F ∈ Fil ⁡ ⋃ J → A ∈ J fClus F ↔ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s
11 1 5 10 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s