Metamath Proof Explorer

Theorem fclstopon

Description: Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclstopon ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ X ↔ F ∈ Fil ⁡ X

Proof

Step Hyp Ref Expression
1 fclstop ⊢ A ∈ J fClus F → J ∈ Top
2 istopon ⊢ J ∈ TopOn ⁡ X ↔ J ∈ Top ∧ X = ⋃ J
3 2 baib ⊢ J ∈ Top → J ∈ TopOn ⁡ X ↔ X = ⋃ J
4 1 3 syl ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ X ↔ X = ⋃ J
5 eqid ⊢ ⋃ J = ⋃ J
6 5 fclsfil ⊢ A ∈ J fClus F → F ∈ Fil ⁡ ⋃ J
7 fveq2 ⊢ X = ⋃ J → Fil ⁡ X = Fil ⁡ ⋃ J
8 7 eleq2d ⊢ X = ⋃ J → F ∈ Fil ⁡ X ↔ F ∈ Fil ⁡ ⋃ J
9 6 8 syl5ibrcom ⊢ A ∈ J fClus F → X = ⋃ J → F ∈ Fil ⁡ X
10 filunibas ⊢ F ∈ Fil ⁡ ⋃ J → ⋃ F = ⋃ J
11 6 10 syl ⊢ A ∈ J fClus F → ⋃ F = ⋃ J
12 filunibas ⊢ F ∈ Fil ⁡ X → ⋃ F = X
13 12 eqeq1d ⊢ F ∈ Fil ⁡ X → ⋃ F = ⋃ J ↔ X = ⋃ J
14 11 13 syl5ibcom ⊢ A ∈ J fClus F → F ∈ Fil ⁡ X → X = ⋃ J
15 9 14 impbid ⊢ A ∈ J fClus F → X = ⋃ J ↔ F ∈ Fil ⁡ X
16 4 15 bitrd ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ X ↔ F ∈ Fil ⁡ X