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 𝑋 = 𝐽
Assertion fclselbas ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴𝑋 )

Proof

Step Hyp Ref Expression
1 fclselbas.1 𝑋 = 𝐽
2 1 fclsfil ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
3 fclstopon ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) )
4 2 3 mpbird ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 fclsopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) ) )
6 4 2 5 syl2anc ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) ) )
7 6 ibi ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴𝑋 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) )
8 7 simpld ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴𝑋 )