flimsncls

Description: If A is a limit point of the filter F , then all the points which specialize A (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015)

		Ref	Expression
	Assertion	flimsncls	$⊢ A \in (J fLim F) \to cls (J) (\{A\}) \subseteq J fLim F$

Proof

Step	Hyp	Ref	Expression
1		flimtop	$⊢ A \in (J fLim F) \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	flimelbas	$⊢ A \in (J fLim F) \to A \in ⋃ J$
4	3	snssd	$⊢ A \in (J fLim F) \to \{A\} \subseteq ⋃ J$
5	2	clsss3	$⊢ (J \in Top \land \{A\} \subseteq ⋃ J) \to cls (J) (\{A\}) \subseteq ⋃ J$
6	1 4 5	syl2anc	$⊢ A \in (J fLim F) \to cls (J) (\{A\}) \subseteq ⋃ J$
7	6	sselda	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to x \in ⋃ J$
8		simpll	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to A \in (J fLim F)$
9	8 1	syl	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to J \in Top$
10		simprl	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to y \in J$
11	1	adantr	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to J \in Top$
12	4	adantr	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to \{A\} \subseteq ⋃ J$
13		simpr	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to x \in cls (J) (\{A\})$
14	11 12 13	3jca	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to (J \in Top \land \{A\} \subseteq ⋃ J \land x \in cls (J) (\{A\}))$
15	2	clsndisj	$⊢ ((J \in Top \land \{A\} \subseteq ⋃ J \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to y \cap \{A\} \neq \emptyset$
16		disjsn	$⊢ y \cap \{A\} = \emptyset \leftrightarrow \neg A \in y$
17	16	necon2abii	$⊢ A \in y \leftrightarrow y \cap \{A\} \neq \emptyset$
18	15 17	sylibr	$⊢ ((J \in Top \land \{A\} \subseteq ⋃ J \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to A \in y$
19	14 18	sylan	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to A \in y$
20		opnneip	$⊢ (J \in Top \land y \in J \land A \in y) \to y \in nei (J) (\{A\})$
21	9 10 19 20	syl3anc	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to y \in nei (J) (\{A\})$
22		flimnei	$⊢ (A \in (J fLim F) \land y \in nei (J) (\{A\})) \to y \in F$
23	8 21 22	syl2anc	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land (y \in J \land x \in y)) \to y \in F$
24	23	expr	$⊢ ((A \in (J fLim F) \land x \in cls (J) (\{A\})) \land y \in J) \to (x \in y \to y \in F)$
25	24	ralrimiva	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to \forall y \in J (x \in y \to y \in F)$
26		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
27	11 26	sylib	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to J \in TopOn (⋃ J)$
28	2	flimfil	$⊢ A \in (J fLim F) \to F \in Fil (⋃ J)$
29	28	adantr	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to F \in Fil (⋃ J)$
30		flimopn	$⊢ (J \in TopOn (⋃ J) \land F \in Fil (⋃ J)) \to (x \in (J fLim F) \leftrightarrow (x \in ⋃ J \land \forall y \in J (x \in y \to y \in F)))$
31	27 29 30	syl2anc	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to (x \in (J fLim F) \leftrightarrow (x \in ⋃ J \land \forall y \in J (x \in y \to y \in F)))$
32	7 25 31	mpbir2and	$⊢ (A \in (J fLim F) \land x \in cls (J) (\{A\})) \to x \in (J fLim F)$
33	32	ex	$⊢ A \in (J fLim F) \to (x \in cls (J) (\{A\}) \to x \in (J fLim F))$
34	33	ssrdv	$⊢ A \in (J fLim F) \to cls (J) (\{A\}) \subseteq J fLim F$

Metamath Proof Explorer

Theorem flimsncls

Proof