Metamath Proof Explorer

Theorem fcfneii

Description: A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	fcfneii	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land (A \in (J fClusf L) (F) \land N \in nei (J) (\{A\}) \land S \in L)) \to N \cap F [S] \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		fcfnei	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset))$
2		ineq1	$⊢ n = N \to n \cap F [s] = N \cap F [s]$
3	2	neeq1d	$⊢ n = N \to (n \cap F [s] \neq \emptyset \leftrightarrow N \cap F [s] \neq \emptyset)$
4		imaeq2	$⊢ s = S \to F [s] = F [S]$
5	4	ineq2d	$⊢ s = S \to N \cap F [s] = N \cap F [S]$
6	5	neeq1d	$⊢ s = S \to (N \cap F [s] \neq \emptyset \leftrightarrow N \cap F [S] \neq \emptyset)$
7	3 6	rspc2v	$⊢ (N \in nei (J) (\{A\}) \land S \in L) \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to N \cap F [S] \neq \emptyset)$
8	7	ex	$⊢ N \in nei (J) (\{A\}) \to (S \in L \to (\forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to N \cap F [S] \neq \emptyset))$
9	8	com3r	$⊢ \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset \to (N \in nei (J) (\{A\}) \to (S \in L \to N \cap F [S] \neq \emptyset))$
10	9	adantl	$⊢ (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in L n \cap F [s] \neq \emptyset) \to (N \in nei (J) (\{A\}) \to (S \in L \to N \cap F [S] \neq \emptyset))$
11	1 10	biimtrdi	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (A \in (J fClusf L) (F) \to (N \in nei (J) (\{A\}) \to (S \in L \to N \cap F [S] \neq \emptyset)))$
12	11	3imp2	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land (A \in (J fClusf L) (F) \land N \in nei (J) (\{A\}) \land S \in L)) \to N \cap F [S] \neq \emptyset$