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