Metamath Proof Explorer

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	\|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A e. X )

Proof

Step	Hyp	Ref	Expression
1		isflf	\|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )
2	1	simprbda	\|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A e. X )

Step

Hyp

Ref

Expression

isflf

 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )

simprbda

 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A e. X )