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