Metamath Proof Explorer

Theorem flfneii

Description: A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	flfneii.x	$⊢ X = ⋃ J$
	Assertion	flfneii	$⊢ ((J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in (J fLimf L) (F) \land N \in nei (J) (\{A\})) \to \exists s \in L F [s] \subseteq N$

Proof

Step	Hyp	Ref	Expression
1		flfneii.x	$⊢ X = ⋃ J$
2	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
3		flfnei	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n))$
4	2 3	syl3an1b	$⊢ (J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fLimf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n))$
5	4	simplbda	$⊢ ((J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in (J fLimf L) (F)) \to \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n$
6	5	3adant3	$⊢ ((J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in (J fLimf L) (F) \land N \in nei (J) (\{A\})) \to \forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n$
7		sseq2	$⊢ n = N \to (F [s] \subseteq n \leftrightarrow F [s] \subseteq N)$
8	7	rexbidv	$⊢ n = N \to (\exists s \in L F [s] \subseteq n \leftrightarrow \exists s \in L F [s] \subseteq N)$
9	8	rspcv	$⊢ N \in nei (J) (\{A\}) \to (\forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n \to \exists s \in L F [s] \subseteq N)$
10	9	3ad2ant3	$⊢ ((J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in (J fLimf L) (F) \land N \in nei (J) (\{A\})) \to (\forall n \in nei (J) (\{A\}) \exists s \in L F [s] \subseteq n \to \exists s \in L F [s] \subseteq N)$
11	6 10	mpd	$⊢ ((J \in Top \land L \in Fil (Y) \land F : Y ⟶ X) \land A \in (J fLimf L) (F) \land N \in nei (J) (\{A\})) \to \exists s \in L F [s] \subseteq N$