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

Metamath Proof Explorer

Theorem flimelbas

Description: A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis flimuni.1 ⊢ 𝑋 = ∪ 𝐽
Assertion flimelbas ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 flimuni.1 ⊢ 𝑋 = ∪ 𝐽
2 1 elflim2 ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
3 2 simprbi ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) )
4 3 simpld ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ 𝑋 )