fclsopn

Description: Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		isfcls2	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fClus F) \leftrightarrow \forall s \in F A \in cls (J) (s))$
2		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
3	2	adantl	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to F \neq \emptyset$
4		r19.2z	$⊢ (F \neq \emptyset \land \forall s \in F A \in cls (J) (s)) \to \exists s \in F A \in cls (J) (s)$
5	4	ex	$⊢ F \neq \emptyset \to (\forall s \in F A \in cls (J) (s) \to \exists s \in F A \in cls (J) (s))$
6	3 5	syl	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (\forall s \in F A \in cls (J) (s) \to \exists s \in F A \in cls (J) (s))$
7		topontop	$⊢ J \in TopOn (X) \to J \in Top$
8	7	ad2antrr	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to J \in Top$
9		filelss	$⊢ (F \in Fil (X) \land s \in F) \to s \subseteq X$
10	9	adantll	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to s \subseteq X$
11		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
12	11	ad2antrr	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to X = ⋃ J$
13	10 12	sseqtrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to s \subseteq ⋃ J$
14		eqid	$⊢ ⋃ J = ⋃ J$
15	14	clsss3	$⊢ (J \in Top \land s \subseteq ⋃ J) \to cls (J) (s) \subseteq ⋃ J$
16	8 13 15	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to cls (J) (s) \subseteq ⋃ J$
17	16 12	sseqtrrd	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to cls (J) (s) \subseteq X$
18	17	sseld	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land s \in F) \to (A \in cls (J) (s) \to A \in X)$
19	18	rexlimdva	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (\exists s \in F A \in cls (J) (s) \to A \in X)$
20	6 19	syld	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (\forall s \in F A \in cls (J) (s) \to A \in X)$
21	20	pm4.71rd	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (\forall s \in F A \in cls (J) (s) \leftrightarrow (A \in X \land \forall s \in F A \in cls (J) (s)))$
22	7	ad3antrrr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to J \in Top$
23	13	adantlr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to s \subseteq ⋃ J$
24		simplr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to A \in X$
25	11	ad3antrrr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to X = ⋃ J$
26	24 25	eleqtrd	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to A \in ⋃ J$
27	14	elcls	$⊢ (J \in Top \land s \subseteq ⋃ J \land A \in ⋃ J) \to (A \in cls (J) (s) \leftrightarrow \forall o \in J (A \in o \to o \cap s \neq \emptyset))$
28	22 23 26 27	syl3anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land s \in F) \to (A \in cls (J) (s) \leftrightarrow \forall o \in J (A \in o \to o \cap s \neq \emptyset))$
29	28	ralbidva	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall s \in F A \in cls (J) (s) \leftrightarrow \forall s \in F \forall o \in J (A \in o \to o \cap s \neq \emptyset))$
30		ralcom	$⊢ \forall s \in F \forall o \in J (A \in o \to o \cap s \neq \emptyset) \leftrightarrow \forall o \in J \forall s \in F (A \in o \to o \cap s \neq \emptyset)$
31		r19.21v	$⊢ \forall s \in F (A \in o \to o \cap s \neq \emptyset) \leftrightarrow (A \in o \to \forall s \in F o \cap s \neq \emptyset)$
32	31	ralbii	$⊢ \forall o \in J \forall s \in F (A \in o \to o \cap s \neq \emptyset) \leftrightarrow \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset)$
33	30 32	bitri	$⊢ \forall s \in F \forall o \in J (A \in o \to o \cap s \neq \emptyset) \leftrightarrow \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset)$
34	29 33	syl6bb	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall s \in F A \in cls (J) (s) \leftrightarrow \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset))$
35	34	pm5.32da	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to ((A \in X \land \forall s \in F A \in cls (J) (s)) \leftrightarrow (A \in X \land \forall o \in J (A \in o \to \forall s \in F o \cap s \neq \emptyset)))$
36	1 21 35	3bitrd	$⊢ (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)))$

Metamath Proof Explorer

Theorem fclsopn

Proof