fclscmpi

Description: Forward direction of fclscmp . Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Hypothesis	flimfnfcls.x	$⊢ X = ⋃ J$
	Assertion	fclscmpi	$⊢ (J \in Comp \land F \in Fil (X)) \to J fClus F \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		flimfnfcls.x	$⊢ X = ⋃ J$
2		cmptop	$⊢ J \in Comp \to J \in Top$
3	1	fclsval	$⊢ (J \in Top \land F \in Fil (X)) \to J fClus F = if (X = X, ⋂_{x \in F} cls (J) (x), \emptyset)$
4		eqid	$⊢ X = X$
5	4	iftruei	$⊢ if (X = X, ⋂_{x \in F} cls (J) (x), \emptyset) = ⋂_{x \in F} cls (J) (x)$
6	3 5	eqtrdi	$⊢ (J \in Top \land F \in Fil (X)) \to J fClus F = ⋂_{x \in F} cls (J) (x)$
7	2 6	sylan	$⊢ (J \in Comp \land F \in Fil (X)) \to J fClus F = ⋂_{x \in F} cls (J) (x)$
8		fvex	$⊢ cls (J) (x) \in V$
9	8	dfiin3	$⊢ ⋂_{x \in F} cls (J) (x) = ⋂ ran (x \in F ⟼ cls (J) (x))$
10	7 9	eqtrdi	$⊢ (J \in Comp \land F \in Fil (X)) \to J fClus F = ⋂ ran (x \in F ⟼ cls (J) (x))$
11		simpl	$⊢ (J \in Comp \land F \in Fil (X)) \to J \in Comp$
12	11	adantr	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to J \in Comp$
13	12 2	syl	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to J \in Top$
14		filelss	$⊢ (F \in Fil (X) \land x \in F) \to x \subseteq X$
15	14	adantll	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to x \subseteq X$
16	1	clscld	$⊢ (J \in Top \land x \subseteq X) \to cls (J) (x) \in Clsd (J)$
17	13 15 16	syl2anc	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to cls (J) (x) \in Clsd (J)$
18	17	fmpttd	$⊢ (J \in Comp \land F \in Fil (X)) \to (x \in F ⟼ cls (J) (x)) : F ⟶ Clsd (J)$
19	18	frnd	$⊢ (J \in Comp \land F \in Fil (X)) \to ran (x \in F ⟼ cls (J) (x)) \subseteq Clsd (J)$
20		simpr	$⊢ (J \in Comp \land F \in Fil (X)) \to F \in Fil (X)$
21	20	adantr	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to F \in Fil (X)$
22		simpr	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to x \in F$
23	1	clsss3	$⊢ (J \in Top \land x \subseteq X) \to cls (J) (x) \subseteq X$
24	13 15 23	syl2anc	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to cls (J) (x) \subseteq X$
25	1	sscls	$⊢ (J \in Top \land x \subseteq X) \to x \subseteq cls (J) (x)$
26	13 15 25	syl2anc	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to x \subseteq cls (J) (x)$
27		filss	$⊢ (F \in Fil (X) \land (x \in F \land cls (J) (x) \subseteq X \land x \subseteq cls (J) (x))) \to cls (J) (x) \in F$
28	21 22 24 26 27	syl13anc	$⊢ ((J \in Comp \land F \in Fil (X)) \land x \in F) \to cls (J) (x) \in F$
29	28	fmpttd	$⊢ (J \in Comp \land F \in Fil (X)) \to (x \in F ⟼ cls (J) (x)) : F ⟶ F$
30	29	frnd	$⊢ (J \in Comp \land F \in Fil (X)) \to ran (x \in F ⟼ cls (J) (x)) \subseteq F$
31		fiss	$⊢ (F \in Fil (X) \land ran (x \in F ⟼ cls (J) (x)) \subseteq F) \to fi (ran (x \in F ⟼ cls (J) (x))) \subseteq fi (F)$
32	20 30 31	syl2anc	$⊢ (J \in Comp \land F \in Fil (X)) \to fi (ran (x \in F ⟼ cls (J) (x))) \subseteq fi (F)$
33		filfi	$⊢ F \in Fil (X) \to fi (F) = F$
34	20 33	syl	$⊢ (J \in Comp \land F \in Fil (X)) \to fi (F) = F$
35	32 34	sseqtrd	$⊢ (J \in Comp \land F \in Fil (X)) \to fi (ran (x \in F ⟼ cls (J) (x))) \subseteq F$
36		0nelfil	$⊢ F \in Fil (X) \to \neg \emptyset \in F$
37	20 36	syl	$⊢ (J \in Comp \land F \in Fil (X)) \to \neg \emptyset \in F$
38	35 37	ssneldd	$⊢ (J \in Comp \land F \in Fil (X)) \to \neg \emptyset \in fi (ran (x \in F ⟼ cls (J) (x)))$
39		cmpfii	$⊢ (J \in Comp \land ran (x \in F ⟼ cls (J) (x)) \subseteq Clsd (J) \land \neg \emptyset \in fi (ran (x \in F ⟼ cls (J) (x)))) \to ⋂ ran (x \in F ⟼ cls (J) (x)) \neq \emptyset$
40	11 19 38 39	syl3anc	$⊢ (J \in Comp \land F \in Fil (X)) \to ⋂ ran (x \in F ⟼ cls (J) (x)) \neq \emptyset$
41	10 40	eqnetrd	$⊢ (J \in Comp \land F \in Fil (X)) \to J fClus F \neq \emptyset$

Metamath Proof Explorer

Theorem fclscmpi

Proof