Theorem 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	⊢ ( 𝜑 → 𝑋 ∈ UFL )
	alexsub.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
	alexsub.3	⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
	alexsub.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
Assertion	alexsub	⊢ ( 𝜑 → 𝐽 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		alexsub.1	⊢ ( 𝜑 → 𝑋 ∈ UFL )
2		alexsub.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
3		alexsub.3	⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
4		alexsub.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
5	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 ∈ UFL )
6	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 = ∪ 𝐵 )
7	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
8	4	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑓 ∈ ( UFil ‘ 𝑋 ) )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ( 𝐽 fLim 𝑓 ) = ∅ )
11	5 6 7 8 9 10	alexsublem	⊢ ¬ ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) )
12	11	pm2.21i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ )
13	12	expr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( ( 𝐽 fLim 𝑓 ) = ∅ → ¬ ( 𝐽 fLim 𝑓 ) = ∅ ) )
14	13	pm2.01d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ )
15	14	neqned	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ )
17		fibas	⊢ ( fi ‘ 𝐵 ) ∈ TopBases
18		tgtopon	⊢ ( ( fi ‘ 𝐵 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
19	17 18	ax-mp	⊢ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) )
20	3 19	eqeltrdi	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
21	1	elexd	⊢ ( 𝜑 → 𝑋 ∈ V )
22	2 21	eqeltrrd	⊢ ( 𝜑 → ∪ 𝐵 ∈ V )
23		uniexb	⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
24	22 23	sylibr	⊢ ( 𝜑 → 𝐵 ∈ V )
25		fiuni	⊢ ( 𝐵 ∈ V → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
26	24 25	syl	⊢ ( 𝜑 → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
27	2 26	eqtrd	⊢ ( 𝜑 → 𝑋 = ∪ ( fi ‘ 𝐵 ) )
28	27	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
29	20 28	eleqtrrd	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
30		ufilcmp	⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
31	1 29 30	syl2anc	⊢ ( 𝜑 → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
32	16 31	mpbird	⊢ ( 𝜑 → 𝐽 ∈ Comp )