Theorem flfelbas

Description: A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

	Ref	Expression
Assertion	flfelbas	$$⊢\left(\left(J\in \mathrm{TopOn}\left(X\right)\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\wedge A\in \left(J\mathrm{fLimf}L\right)\left(F\right)\right)\to A\in X$$

Proof

Step	Hyp	Ref	Expression
1		isflf	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\to \left(A\in \left(J\mathrm{fLimf}L\right)\left(F\right)\leftrightarrow \left(A\in X\wedge \forall o\in J\left(A\in o\to \exists s\in LF\left[s\right]\subseteq o\right)\right)\right)$$
2	1	simprbda	$$⊢\left(\left(J\in \mathrm{TopOn}\left(X\right)\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\wedge A\in \left(J\mathrm{fLimf}L\right)\left(F\right)\right)\to A\in X$$