fclsbas

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

		Ref	Expression
	Hypothesis	fclsbas.f	$⊢ F = X filGen B$
	Assertion	fclsbas	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in B o \cap s \neq \emptyset)))$

Proof

Step	Hyp	Ref	Expression
1		fclsbas.f	$⊢ F = X filGen B$
2		fgcl	$⊢ B \in fBas (X) \to X filGen B \in Fil (X)$
3	2	adantl	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to X filGen B \in Fil (X)$
4	1 3	eqeltrid	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to F \in Fil (X)$
5		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 t \in F o \cap t \neq \emptyset)))$
6	4 5	syldan	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall t \in F o \cap t \neq \emptyset)))$
7		ssfg	$⊢ B \in fBas (X) \to B \subseteq X filGen B$
8	7	ad3antlr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to B \subseteq X filGen B$
9	8 1	sseqtrrdi	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to B \subseteq F$
10		ssralv	$⊢ B \subseteq F \to (\forall t \in F o \cap t \neq \emptyset \to \forall t \in B o \cap t \neq \emptyset)$
11	9 10	syl	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (\forall t \in F o \cap t \neq \emptyset \to \forall t \in B o \cap t \neq \emptyset)$
12		ineq2	$⊢ t = s \to o \cap t = o \cap s$
13	12	neeq1d	$⊢ t = s \to (o \cap t \neq \emptyset \leftrightarrow o \cap s \neq \emptyset)$
14	13	cbvralvw	$⊢ \forall t \in B o \cap t \neq \emptyset \leftrightarrow \forall s \in B o \cap s \neq \emptyset$
15	11 14	syl6ib	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (\forall t \in F o \cap t \neq \emptyset \to \forall s \in B o \cap s \neq \emptyset)$
16	1	eleq2i	$⊢ t \in F \leftrightarrow t \in (X filGen B)$
17		elfg	$⊢ B \in fBas (X) \to (t \in (X filGen B) \leftrightarrow (t \subseteq X \land \exists s \in B s \subseteq t))$
18	17	ad3antlr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (t \in (X filGen B) \leftrightarrow (t \subseteq X \land \exists s \in B s \subseteq t))$
19	16 18	syl5bb	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (t \in F \leftrightarrow (t \subseteq X \land \exists s \in B s \subseteq t))$
20	19	simplbda	$⊢ ((((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \land t \in F) \to \exists s \in B s \subseteq t$
21		r19.29r	$⊢ (\exists s \in B s \subseteq t \land \forall s \in B o \cap s \neq \emptyset) \to \exists s \in B (s \subseteq t \land o \cap s \neq \emptyset)$
22		sslin	$⊢ s \subseteq t \to o \cap s \subseteq o \cap t$
23		ssn0	$⊢ (o \cap s \subseteq o \cap t \land o \cap s \neq \emptyset) \to o \cap t \neq \emptyset$
24	22 23	sylan	$⊢ (s \subseteq t \land o \cap s \neq \emptyset) \to o \cap t \neq \emptyset$
25	24	rexlimivw	$⊢ \exists s \in B (s \subseteq t \land o \cap s \neq \emptyset) \to o \cap t \neq \emptyset$
26	21 25	syl	$⊢ (\exists s \in B s \subseteq t \land \forall s \in B o \cap s \neq \emptyset) \to o \cap t \neq \emptyset$
27	26	ex	$⊢ \exists s \in B s \subseteq t \to (\forall s \in B o \cap s \neq \emptyset \to o \cap t \neq \emptyset)$
28	20 27	syl	$⊢ ((((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \land t \in F) \to (\forall s \in B o \cap s \neq \emptyset \to o \cap t \neq \emptyset)$
29	28	ralrimdva	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (\forall s \in B o \cap s \neq \emptyset \to \forall t \in F o \cap t \neq \emptyset)$
30	15 29	impbid	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (o \in J \land A \in o)) \to (\forall t \in F o \cap t \neq \emptyset \leftrightarrow \forall s \in B o \cap s \neq \emptyset)$
31	30	anassrs	$⊢ ((((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land o \in J) \land A \in o) \to (\forall t \in F o \cap t \neq \emptyset \leftrightarrow \forall s \in B o \cap s \neq \emptyset)$
32	31	pm5.74da	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land o \in J) \to ((A \in o \to \forall t \in F o \cap t \neq \emptyset) \leftrightarrow (A \in o \to \forall s \in B o \cap s \neq \emptyset))$
33	32	ralbidva	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall o \in J (A \in o \to \forall t \in F o \cap t \neq \emptyset) \leftrightarrow \forall o \in J (A \in o \to \forall s \in B o \cap s \neq \emptyset))$
34	33	pm5.32da	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to ((A \in X \land \forall o \in J (A \in o \to \forall t \in F o \cap t \neq \emptyset)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in B o \cap s \neq \emptyset)))$
35	6 34	bitrd	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fClus F) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in B o \cap s \neq \emptyset)))$

Metamath Proof Explorer

Theorem fclsbas

Proof