fclsnei

Description: Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Assertion	fclsnei	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	fclselbas	$⊢ A \in (J fClus F) \to A \in ⋃ J$
3		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
4	3	adantr	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to X = ⋃ J$
5	4	eleq2d	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in X \leftrightarrow A \in ⋃ J)$
6	2 5	syl5ibr	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \to A \in X)$
7		fclsneii	$⊢ (A \in (J fClus F) \land n \in nei (J) (\{A\}) \land s \in F) \to n \cap s \neq \emptyset$
8	7	3expb	$⊢ (A \in (J fClus F) \land (n \in nei (J) (\{A\}) \land s \in F)) \to n \cap s \neq \emptyset$
9	8	ralrimivva	$⊢ A \in (J fClus F) \to \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset$
10	6 9	jca2	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \to (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset))$
11		topontop	$⊢ J \in TopOn (X) \to J \in Top$
12	11	ad3antrrr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (o \in J \land A \in o)) \to J \in Top$
13		simprl	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (o \in J \land A \in o)) \to o \in J$
14		simprr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (o \in J \land A \in o)) \to A \in o$
15		opnneip	$⊢ (J \in Top \land o \in J \land A \in o) \to o \in nei (J) (\{A\})$
16	12 13 14 15	syl3anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (o \in J \land A \in o)) \to o \in nei (J) (\{A\})$
17		ineq1	$⊢ n = o \to n \cap s = o \cap s$
18	17	neeq1d	$⊢ n = o \to (n \cap s \neq \emptyset \leftrightarrow o \cap s \neq \emptyset)$
19	18	ralbidv	$⊢ n = o \to (\forall s \in F n \cap s \neq \emptyset \leftrightarrow \forall s \in F o \cap s \neq \emptyset)$
20	19	rspcv	$⊢ o \in nei (J) (\{A\}) \to (\forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset \to \forall s \in F o \cap s \neq \emptyset)$
21	16 20	syl	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (o \in J \land A \in o)) \to (\forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset \to \forall s \in F o \cap s \neq \emptyset)$
22	21	expr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land o \in J) \to (A \in o \to (\forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset \to \forall s \in F o \cap s \neq \emptyset))$
23	22	com23	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land o \in J) \to (\forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset \to (A \in o \to \forall s \in F o \cap s \neq \emptyset))$
24	23	ralrimdva	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset \to \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset))$
25	24	imdistanda	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to ((A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset) \to (A \in X \land \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset)))$
26		fclsopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset)))$
27	25 26	sylibrd	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to ((A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset) \to A \in (J fClus F))$
28	10 27	impbid	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \forall s \in F n \cap s \neq \emptyset))$

Metamath Proof Explorer

Theorem fclsnei

Proof