Metamath Proof Explorer


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 )