Metamath Proof Explorer

Theorem fcfelbas

Description: A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfelbas ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F → A ∈ X

Proof

Step Hyp Ref Expression
1 fcfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fClus X FilMap F ⁡ L
2 1 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fClusf L ⁡ F ↔ A ∈ J fClus X FilMap F ⁡ L
3 eqid ⊢ ⋃ J = ⋃ J
4 3 fclselbas ⊢ A ∈ J fClus X FilMap F ⁡ L → A ∈ ⋃ J
5 2 4 syl6bi ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → A ∈ J fClusf L ⁡ F → A ∈ ⋃ J
6 5 imp ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F → A ∈ ⋃ J
7 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F → J ∈ TopOn ⁡ X
8 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
9 7 8 syl ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F → X = ⋃ J
10 6 9 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X ∧ A ∈ J fClusf L ⁡ F → A ∈ X