fclsneii

Description: A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Assertion	fclsneii	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to N \cap S \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to A \in (J fClus F)$
2		fclstop	$⊢ A \in (J fClus F) \to J \in Top$
3	1 2	syl	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to J \in Top$
4		simp2	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to N \in nei (J) (\{A\})$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5	neii1	$⊢ (J \in Top \land N \in nei (J) (\{A\})) \to N \subseteq ⋃ J$
7	3 4 6	syl2anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to N \subseteq ⋃ J$
8	5	ntrss2	$⊢ (J \in Top \land N \subseteq ⋃ J) \to int (J) (N) \subseteq N$
9	3 7 8	syl2anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to int (J) (N) \subseteq N$
10	9	ssrind	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to int (J) (N) \cap S \subseteq N \cap S$
11	5	ntropn	$⊢ (J \in Top \land N \subseteq ⋃ J) \to int (J) (N) \in J$
12	3 7 11	syl2anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to int (J) (N) \in J$
13	5	fclselbas	$⊢ A \in (J fClus F) \to A \in ⋃ J$
14	1 13	syl	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to A \in ⋃ J$
15	14	snssd	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to \{A\} \subseteq ⋃ J$
16	5	neiint	$⊢ (J \in Top \land \{A\} \subseteq ⋃ J \land N \subseteq ⋃ J) \to (N \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (N))$
17	3 15 7 16	syl3anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to (N \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (N))$
18	4 17	mpbid	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to \{A\} \subseteq int (J) (N)$
19		snssg	$⊢ A \in ⋃ J \to (A \in int (J) (N) \leftrightarrow \{A\} \subseteq int (J) (N))$
20	14 19	syl	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to (A \in int (J) (N) \leftrightarrow \{A\} \subseteq int (J) (N))$
21	18 20	mpbird	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to A \in int (J) (N)$
22		simp3	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to S \in F$
23		fclsopni	$⊢ (A \in (J fClus F) \land (int (J) (N) \in J \land A \in int (J) (N) \land S \in F)) \to int (J) (N) \cap S \neq \emptyset$
24	1 12 21 22 23	syl13anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to int (J) (N) \cap S \neq \emptyset$
25		ssn0	$⊢ (int (J) (N) \cap S \subseteq N \cap S \land int (J) (N) \cap S \neq \emptyset) \to N \cap S \neq \emptyset$
26	10 24 25	syl2anc	$⊢ (A \in (J fClus F) \land N \in nei (J) (\{A\}) \land S \in F) \to N \cap S \neq \emptyset$

Metamath Proof Explorer

Theorem fclsneii

Proof