fclscmp

Description: A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Assertion	fclscmp	$⊢ J \in TopOn (X) \to (J \in Comp \leftrightarrow \forall f \in Fil (X) J fClus f \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	fclscmpi	$⊢ (J \in Comp \land f \in Fil (⋃ J)) \to J fClus f \neq \emptyset$
3	2	ralrimiva	$⊢ J \in Comp \to \forall f \in Fil (⋃ J) J fClus f \neq \emptyset$
4		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
5	4	fveq2d	$⊢ J \in TopOn (X) \to Fil (X) = Fil (⋃ J)$
6	5	raleqdv	$⊢ J \in TopOn (X) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \leftrightarrow \forall f \in Fil (⋃ J) J fClus f \neq \emptyset)$
7	3 6	imbitrrid	$⊢ J \in TopOn (X) \to (J \in Comp \to \forall f \in Fil (X) J fClus f \neq \emptyset)$
8		elpwi	$⊢ x \in 𝒫 Clsd (J) \to x \subseteq Clsd (J)$
9		vn0	$⊢ V \neq \emptyset$
10		simpr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to x = \emptyset$
11	10	inteqd	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to ⋂ x = ⋂ \emptyset$
12		int0	$⊢ ⋂ \emptyset = V$
13	11 12	eqtrdi	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to ⋂ x = V$
14	13	neeq1d	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to (⋂ x \neq \emptyset \leftrightarrow V \neq \emptyset)$
15	9 14	mpbiri	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to ⋂ x \neq \emptyset$
16	15	a1d	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x = \emptyset) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to ⋂ x \neq \emptyset)$
17		ssfii	$⊢ x \in V \to x \subseteq fi (x)$
18	17	elv	$⊢ x \subseteq fi (x)$
19		simplrl	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to x \subseteq Clsd (J)$
20	1	cldss2	$⊢ Clsd (J) \subseteq 𝒫 ⋃ J$
21	4	ad2antrr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to X = ⋃ J$
22	21	pweqd	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to 𝒫 X = 𝒫 ⋃ J$
23	20 22	sseqtrrid	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to Clsd (J) \subseteq 𝒫 X$
24	19 23	sstrd	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to x \subseteq 𝒫 X$
25		simpr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to x \neq \emptyset$
26		simplrr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to \neg \emptyset \in fi (x)$
27		toponmax	$⊢ J \in TopOn (X) \to X \in J$
28	27	ad2antrr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to X \in J$
29		fsubbas	$⊢ X \in J \to (fi (x) \in fBas (X) \leftrightarrow (x \subseteq 𝒫 X \land x \neq \emptyset \land \neg \emptyset \in fi (x)))$
30	28 29	syl	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to (fi (x) \in fBas (X) \leftrightarrow (x \subseteq 𝒫 X \land x \neq \emptyset \land \neg \emptyset \in fi (x)))$
31	24 25 26 30	mpbir3and	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to fi (x) \in fBas (X)$
32		ssfg	$⊢ fi (x) \in fBas (X) \to fi (x) \subseteq X filGen fi (x)$
33	31 32	syl	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to fi (x) \subseteq X filGen fi (x)$
34	18 33	sstrid	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to x \subseteq X filGen fi (x)$
35	34	sselda	$⊢ (((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \land y \in x) \to y \in (X filGen fi (x))$
36		fclssscls	$⊢ y \in (X filGen fi (x)) \to J fClus (X filGen fi (x)) \subseteq cls (J) (y)$
37	35 36	syl	$⊢ (((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \land y \in x) \to J fClus (X filGen fi (x)) \subseteq cls (J) (y)$
38	19	sselda	$⊢ (((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \land y \in x) \to y \in Clsd (J)$
39		cldcls	$⊢ y \in Clsd (J) \to cls (J) (y) = y$
40	38 39	syl	$⊢ (((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \land y \in x) \to cls (J) (y) = y$
41	37 40	sseqtrd	$⊢ (((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \land y \in x) \to J fClus (X filGen fi (x)) \subseteq y$
42	41	ralrimiva	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to \forall y \in x J fClus (X filGen fi (x)) \subseteq y$
43		ssint	$⊢ J fClus (X filGen fi (x)) \subseteq ⋂ x \leftrightarrow \forall y \in x J fClus (X filGen fi (x)) \subseteq y$
44	42 43	sylibr	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to J fClus (X filGen fi (x)) \subseteq ⋂ x$
45		fgcl	$⊢ fi (x) \in fBas (X) \to X filGen fi (x) \in Fil (X)$
46		oveq2	$⊢ f = X filGen fi (x) \to J fClus f = J fClus (X filGen fi (x))$
47	46	neeq1d	$⊢ f = X filGen fi (x) \to (J fClus f \neq \emptyset \leftrightarrow J fClus (X filGen fi (x)) \neq \emptyset)$
48	47	rspcv	$⊢ X filGen fi (x) \in Fil (X) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to J fClus (X filGen fi (x)) \neq \emptyset)$
49	31 45 48	3syl	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to J fClus (X filGen fi (x)) \neq \emptyset)$
50		ssn0	$⊢ (J fClus (X filGen fi (x)) \subseteq ⋂ x \land J fClus (X filGen fi (x)) \neq \emptyset) \to ⋂ x \neq \emptyset$
51	44 49 50	syl6an	$⊢ ((J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \land x \neq \emptyset) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to ⋂ x \neq \emptyset)$
52	16 51	pm2.61dane	$⊢ (J \in TopOn (X) \land (x \subseteq Clsd (J) \land \neg \emptyset \in fi (x))) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to ⋂ x \neq \emptyset)$
53	52	expr	$⊢ (J \in TopOn (X) \land x \subseteq Clsd (J)) \to (\neg \emptyset \in fi (x) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to ⋂ x \neq \emptyset))$
54	8 53	sylan2	$⊢ (J \in TopOn (X) \land x \in 𝒫 Clsd (J)) \to (\neg \emptyset \in fi (x) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to ⋂ x \neq \emptyset))$
55	54	com23	$⊢ (J \in TopOn (X) \land x \in 𝒫 Clsd (J)) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$
56	55	ralrimdva	$⊢ J \in TopOn (X) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$
57		topontop	$⊢ J \in TopOn (X) \to J \in Top$
58		cmpfi	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$
59	57 58	syl	$⊢ J \in TopOn (X) \to (J \in Comp \leftrightarrow \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$
60	56 59	sylibrd	$⊢ J \in TopOn (X) \to (\forall f \in Fil (X) J fClus f \neq \emptyset \to J \in Comp)$
61	7 60	impbid	$⊢ J \in TopOn (X) \to (J \in Comp \leftrightarrow \forall f \in Fil (X) J fClus f \neq \emptyset)$

Metamath Proof Explorer

Theorem fclscmp

Proof