Metamath Proof Explorer

Theorem fclselbas

Description: A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis fclselbas.1 ⊢ X = ⋃ J
Assertion fclselbas ⊢ A ∈ J fClus F → A ∈ X

Proof

Step Hyp Ref Expression
1 fclselbas.1 ⊢ X = ⋃ J
2 1 fclsfil ⊢ A ∈ J fClus F → F ∈ Fil ⁡ X
3 fclstopon ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ X ↔ F ∈ Fil ⁡ X
4 2 3 mpbird ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ X
5 fclsopn ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅
6 4 2 5 syl2anc ⊢ A ∈ J fClus F → A ∈ J fClus F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅
7 6 ibi ⊢ A ∈ J fClus F → A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅
8 7 simpld ⊢ A ∈ J fClus F → A ∈ X