alexsub

Description: The Alexander Subbase Theorem: If B is a subbase for the topology J , and any cover taken from B has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010) (Revised by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	alexsub.1	$⊢ φ \to X \in UFL$
	alexsub.2	$⊢ φ \to X = ⋃ B$
	alexsub.3	$⊢ φ \to J = topGen (fi (B))$
	alexsub.4	$⊢ (φ \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
Assertion	alexsub	$⊢ φ \to J \in Comp$

Proof

Step	Hyp	Ref	Expression
1		alexsub.1	$⊢ φ \to X \in UFL$
2		alexsub.2	$⊢ φ \to X = ⋃ B$
3		alexsub.3	$⊢ φ \to J = topGen (fi (B))$
4		alexsub.4	$⊢ (φ \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
5	1	adantr	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to X \in UFL$
6	2	adantr	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to X = ⋃ B$
7	3	adantr	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to J = topGen (fi (B))$
8	4	adantlr	$⊢ ((φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
9		simprl	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to f \in UFil (X)$
10		simprr	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to J fLim f = \emptyset$
11	5 6 7 8 9 10	alexsublem	$⊢ \neg (φ \land (f \in UFil (X) \land J fLim f = \emptyset))$
12	11	pm2.21i	$⊢ (φ \land (f \in UFil (X) \land J fLim f = \emptyset)) \to \neg J fLim f = \emptyset$
13	12	expr	$⊢ (φ \land f \in UFil (X)) \to (J fLim f = \emptyset \to \neg J fLim f = \emptyset)$
14	13	pm2.01d	$⊢ (φ \land f \in UFil (X)) \to \neg J fLim f = \emptyset$
15	14	neqned	$⊢ (φ \land f \in UFil (X)) \to J fLim f \neq \emptyset$
16	15	ralrimiva	$⊢ φ \to \forall f \in UFil (X) J fLim f \neq \emptyset$
17		fibas	$⊢ fi (B) \in TopBases$
18		tgtopon	$⊢ fi (B) \in TopBases \to topGen (fi (B)) \in TopOn (⋃ fi (B))$
19	17 18	ax-mp	$⊢ topGen (fi (B)) \in TopOn (⋃ fi (B))$
20	3 19	eqeltrdi	$⊢ φ \to J \in TopOn (⋃ fi (B))$
21	1	elexd	$⊢ φ \to X \in V$
22	2 21	eqeltrrd	$⊢ φ \to ⋃ B \in V$
23		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
24	22 23	sylibr	$⊢ φ \to B \in V$
25		fiuni	$⊢ B \in V \to ⋃ B = ⋃ fi (B)$
26	24 25	syl	$⊢ φ \to ⋃ B = ⋃ fi (B)$
27	2 26	eqtrd	$⊢ φ \to X = ⋃ fi (B)$
28	27	fveq2d	$⊢ φ \to TopOn (X) = TopOn (⋃ fi (B))$
29	20 28	eleqtrrd	$⊢ φ \to J \in TopOn (X)$
30		ufilcmp	$⊢ (X \in UFL \land J \in TopOn (X)) \to (J \in Comp \leftrightarrow \forall f \in UFil (X) J fLim f \neq \emptyset)$
31	1 29 30	syl2anc	$⊢ φ \to (J \in Comp \leftrightarrow \forall f \in UFil (X) J fLim f \neq \emptyset)$
32	16 31	mpbird	$⊢ φ \to J \in Comp$

Metamath Proof Explorer

Theorem alexsub

Proof