This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ) → 𝐴 ∈ 𝑋 )