ufilcmp

Description: A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009) (Proof shortened by Mario Carneiro, 12-Apr-2015) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	ufilcmp	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \leftrightarrow \forall f \in UFil (X) J fLim f \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ f \in UFil (⋃ J) \to f \in Fil (⋃ J)$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	fclscmpi	$⊢ (J \in Comp \land f \in Fil (⋃ J)) \to J fClus f \neq \emptyset$
4	1 3	sylan2	$⊢ (J \in Comp \land f \in UFil (⋃ J)) \to J fClus f \neq \emptyset$
5	4	ralrimiva	$⊢ J \in Comp \to \forall f \in UFil (⋃ J) J fClus f \neq \emptyset$
6		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
7	6	fveq2d	$⊢ J \in TopOn (X) \to UFil (X) = UFil (⋃ J)$
8	7	raleqdv	$⊢ J \in TopOn (X) \to (\forall f \in UFil (X) J fClus f \neq \emptyset \leftrightarrow \forall f \in UFil (⋃ J) J fClus f \neq \emptyset)$
9	8	adantl	$⊢ (X \in UFL \land J \in TopOn (X)) \to (\forall f \in UFil (X) J fClus f \neq \emptyset \leftrightarrow \forall f \in UFil (⋃ J) J fClus f \neq \emptyset)$
10	5 9	imbitrrid	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \to \forall f \in UFil (X) J fClus f \neq \emptyset)$
11		ufli	$⊢ (X \in UFL \land g \in Fil (X)) \to \exists f \in UFil (X) g \subseteq f$
12	11	adantlr	$⊢ ((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \to \exists f \in UFil (X) g \subseteq f$
13		r19.29	$⊢ (\forall f \in UFil (X) J fClus f \neq \emptyset \land \exists f \in UFil (X) g \subseteq f) \to \exists f \in UFil (X) (J fClus f \neq \emptyset \land g \subseteq f)$
14		simpllr	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land (f \in UFil (X) \land g \subseteq f)) \to J \in TopOn (X)$
15		simplr	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land (f \in UFil (X) \land g \subseteq f)) \to g \in Fil (X)$
16		simprr	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land (f \in UFil (X) \land g \subseteq f)) \to g \subseteq f$
17		fclsss2	$⊢ (J \in TopOn (X) \land g \in Fil (X) \land g \subseteq f) \to J fClus f \subseteq J fClus g$
18	14 15 16 17	syl3anc	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land (f \in UFil (X) \land g \subseteq f)) \to J fClus f \subseteq J fClus g$
19		ssn0	$⊢ (J fClus f \subseteq J fClus g \land J fClus f \neq \emptyset) \to J fClus g \neq \emptyset$
20	19	ex	$⊢ J fClus f \subseteq J fClus g \to (J fClus f \neq \emptyset \to J fClus g \neq \emptyset)$
21	18 20	syl	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land (f \in UFil (X) \land g \subseteq f)) \to (J fClus f \neq \emptyset \to J fClus g \neq \emptyset)$
22	21	expr	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land f \in UFil (X)) \to (g \subseteq f \to (J fClus f \neq \emptyset \to J fClus g \neq \emptyset))$
23	22	impcomd	$⊢ (((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \land f \in UFil (X)) \to ((J fClus f \neq \emptyset \land g \subseteq f) \to J fClus g \neq \emptyset)$
24	23	rexlimdva	$⊢ ((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \to (\exists f \in UFil (X) (J fClus f \neq \emptyset \land g \subseteq f) \to J fClus g \neq \emptyset)$
25	13 24	syl5	$⊢ ((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \to ((\forall f \in UFil (X) J fClus f \neq \emptyset \land \exists f \in UFil (X) g \subseteq f) \to J fClus g \neq \emptyset)$
26	12 25	mpan2d	$⊢ ((X \in UFL \land J \in TopOn (X)) \land g \in Fil (X)) \to (\forall f \in UFil (X) J fClus f \neq \emptyset \to J fClus g \neq \emptyset)$
27	26	ralrimdva	$⊢ (X \in UFL \land J \in TopOn (X)) \to (\forall f \in UFil (X) J fClus f \neq \emptyset \to \forall g \in Fil (X) J fClus g \neq \emptyset)$
28		fclscmp	$⊢ J \in TopOn (X) \to (J \in Comp \leftrightarrow \forall g \in Fil (X) J fClus g \neq \emptyset)$
29	28	adantl	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \leftrightarrow \forall g \in Fil (X) J fClus g \neq \emptyset)$
30	27 29	sylibrd	$⊢ (X \in UFL \land J \in TopOn (X)) \to (\forall f \in UFil (X) J fClus f \neq \emptyset \to J \in Comp)$
31	10 30	impbid	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \leftrightarrow \forall f \in UFil (X) J fClus f \neq \emptyset)$
32		uffclsflim	$⊢ f \in UFil (X) \to J fClus f = J fLim f$
33	32	neeq1d	$⊢ f \in UFil (X) \to (J fClus f \neq \emptyset \leftrightarrow J fLim f \neq \emptyset)$
34	33	ralbiia	$⊢ \forall f \in UFil (X) J fClus f \neq \emptyset \leftrightarrow \forall f \in UFil (X) J fLim f \neq \emptyset$
35	31 34	bitrdi	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \leftrightarrow \forall f \in UFil (X) J fLim f \neq \emptyset)$

Metamath Proof Explorer

Theorem ufilcmp

Proof